Cited references
References that are explicitly cited from the design documents, papers, or guides. The single source of truth for \cite{...} calls in the LaTeX papers; new entries follow the same lowercase-key convention.
Generated from docs/references/eigenius.bib by scripts/bib-to-md.py. Do not edit by hand.
Total entries: 61.
agda
Norell, Ulf (2009). “Dependently typed programming in Agda”. In Advanced Functional Programming, AFP 2008, Lecture Notes in Computer Science 5832, pp. 230–266, Springer.
aiguier-diaconescu2007
Aiguier, Marc and Diaconescu, Răzvan (2007). “Stratified institutions and elementary homomorphisms”. Information Processing Letters, 103(1), pp. 5–13.
DOI: 10.1016/j.ipl.2007.02.005
alice
Abiteboul, Serge, Hull, Richard, and Vianu, Victor (1995). Foundations of Databases. Addison-Wesley.
atomicdata
Meindertsma, Joep (2020–2026). Atomic Data: A modular specification for sharing, modifying and modeling graph data.
W3C Community Group Specification
basold2016
Basold, Henning and Geuvers, Herman (2016). “Type theory based on dependent inductive and coinductive types”. In LICS 2016: 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 327–336, ACM.
cafeobj
Diaconescu, Răzvan and Futatsugi, Kokichi (1998). CafeOBJ Report. AMAST Series in Computing, vol. 6, World Scientific.
cargo-component
Bytecode Alliance. cargo-component: A Cargo subcommand for building WebAssembly components.
Software
carneiro2024
Carneiro, Mario (2024). Lean4Lean: Verifying a Typechecker for Lean, in Lean.
cbor-x
Loup, Kris. cbor-x: CBOR encoder/decoder for JavaScript.
Software (npm package)
cwl
Amstutz, Peter, et al. (2022). Common Workflow Language, v1.2.
dapr
Dapr Authors. Dapr: Distributed Application Runtime.
Cloud Native Computing Foundation graduated project
deepproblog
Manhaeve, Robin, Dumančić, Sebastijan, Kimmig, Angelika, Demeester, Thomas, and De Raedt, Luc (2018). “DeepProbLog: Neural probabilistic logic programming”. In NeurIPS 2018: 32nd Conference on Neural Information Processing Systems.
deno
Deno Land Inc.. Deno: A modern runtime for JavaScript and TypeScript.
Software
diaconescu-iep
Diaconescu, Răzvan (2016). Institution Theory. Internet Encyclopedia of Philosophy.
Survey article; provides the canonical encyclopedic introduction to institution theory.
diaconescu-madeira2016
Diaconescu, Răzvan and Madeira, Alexandre (2016). “Encoding hybridized institutions into first-order logic”. Mathematical Structures in Computer Science, 26(5), pp. 745–788.
DOI: 10.1017/S0960129514000383
diaconescu2002
Diaconescu, Răzvan (2002). “Grothendieck institutions”. Applied Categorical Structures, 10(4), pp. 383–402.
diaconescu2008
Diaconescu, Răzvan (2008). Institution-independent Model Theory. Birkhäuser, Basel.
First edition. For citations to specific chapters, theorems, or page numbers, prefer the second edition (\textttdiaconescu2025), which has revised numbering.
diaconescu2012-three-decades
Diaconescu, Răzvan (2012). “Three decades of institution theory”. In Universal Logic: An Anthology, ed. Béziau, Jean-Yves, Studies in Universal Logic, pp. 309–322, Birkhäuser.
DOI: 10.1007/978-3-0346-0145-0_25
diaconescu2017-3half-institutions
Diaconescu, Răzvan (2017). 3/2-Institutions: An institution theory for conceptual blending.
Extension of institution theory accommodating implicit partiality of signature morphisms; motivated by conceptual blending and software evolution.
diaconescu2025
Diaconescu, Răzvan (2025). Institution-independent Model Theory. Studies in Universal Logic, Springer Nature Switzerland.
DOI: 10.1007/978-3-031-68854-6
Second edition. Chapter 14 (`Grothendieck institutions’, pp. 449–473) is the canonical reference for the Grothendieck construction on institutions, the comorphism-based variant, and the globalisation theorems for theory co-limits, model amalgamation (Thm. 14.15) and interpolation (Thm. 14.16).
goguen-burstall1984
Goguen, Joseph A. and Burstall, Rod M. (1984). “Introducing institutions”. In Logics of Programs: Workshop, Carnegie Mellon University, Pittsburgh, PA, June 6–8, 1983, ed. Clarke, Edmund and Kozen, Dexter, Lecture Notes in Computer Science 164, pp. 221–256, Springer.
DOI: 10.1007/3-540-12896-4_366
goguen-rosu2002
Goguen, Joseph A. and Roşu, Grigore (2002). “Institution morphisms”. Formal Aspects of Computing, 13(3—5), pp. 274–307.
Special issue dedicated to Rod Burstall on his retirement.
goguen1992
Goguen, Joseph A. and Burstall, Rod M. (1992). “Institutions: Abstract model theory for specification and programming”. Journal of the ACM, 39(1), pp. 95–146.
hancock-setzer2000
Hancock, Peter and Setzer, Anton (2000). “Interactive programs in dependent type theory”. In Computer Science Logic, CSL 2000, Lecture Notes in Computer Science 1862, pp. 317–331, Springer.
idris
Brady, Edwin (2021). “Idris 2: Quantitative type theory in practice”. In ECOOP 2021: 35th European Conference on Object-Oriented Programming, LIPIcs 194.
langchain
Chase, Harrison (2023). LangChain.
lean4
de Moura, Leonardo and Ullrich, Sebastian (2021). “The Lean 4 theorem prover and programming language”. In CADE-28: 28th International Conference on Automated Deduction, Lecture Notes in Computer Science 12699, pp. 625–635, Springer.
lean4export
The Lean Prover Community. lean4export: Reference exporter for the Lean 4 kernel export format.
Software
lean4lean
Carneiro, Mario. Lean4Lean: A type checker for Lean 4, written in Lean 4.
Software; companion to \citecarneiro2024
llamaindex
Liu, Jerry (2023). LlamaIndex.
ltn
Badreddine, Samy, Garcez, Artur d’Avila, Serafini, Luciano, and Spranger, Michael (2022). “Logic tensor networks”. Artificial Intelligence, 303.
meseguer1989
Meseguer, José (1989). “General logics”. In Logic Colloquium ‘87, ed. Ebbinghaus, H.-D., Fernandez-Prida, J., Garrido, M., Lascar, D., and Artalejo, M. R., Studies in Logic and the Foundations of Mathematics 129, pp. 275–329, Elsevier.
minitt
Coquand, Thierry, Kinoshita, Yoshiki, Nordström, Bengt, and Takeyama, Makoto (2009). “A simple type-theoretic language: EigenTT”. In From Semantics to Computer Science: Essays in Honour of Gilles Kahn, ed. Bertot, Yves, Huet, Gérard, Lévy, Jean-Jacques, and Plotkin, Gordon, pp. 139–164, Cambridge University Press.
mossakowski2007hets
Mossakowski, Till, Maeder, Christian, and Lüttich, Klaus (2007). “The heterogeneous tool set, Hets”. In TACAS 2007: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 4424, pp. 519–522, Springer.
mossakowski2015dol
Mossakowski, Till, Codescu, Mihai, Neuhaus, Fabian, and Kutz, Oliver (2015). “The Distributed Ontology, Modeling, and Specification Language — DOL”. In The Road to Universal Logic, Volume II: Festschrift for the 50th Birthday of Jean-Yves Béziau, ed. Koslow, Arnold and Buchsbaum, Arthur, Studies in Universal Logic, pp. 489–520, Birkhäuser/Springer.
DOI: 10.1007/978-3-319-15368-1_21
Companion paper to the OMG DOL standard (\citeontoiop); surveys the language and its institution-theoretic foundation.
nanoda_lib
Bailey, Chris. nanoda_lib: A Lean 4 term checker library in Rust.
Software
nbe
Abel, Andreas, Coquand, Thierry, and Dybjer, Peter (2007). “Normalization by evaluation for Martin-Löf type theory with typed equality judgements”. In LICS 2007: 22nd Annual IEEE Symposium on Logic in Computer Science, pp. 3–12, IEEE.
neurasp
Yang, Zhun, Ishay, Adam, and Lee, Joohyung (2020). “NeurASP: Embracing neural networks into answer set programming”. In IJCAI 2020: 29th International Joint Conference on Artificial Intelligence.
ontoiop
Object Management Group (2018). “Distributed Ontology, Modeling and Specification Language (DOL), Version 1.0”. OMG, formal/2018-08-01.
owl
Hitzler, Pascal, Krötzsch, Markus, Parsia, Bijan, Patel-Schneider, Peter F., and Rudolph, Sebastian (2012). “OWL 2 Web Ontology Language Primer”. W3C, W3C Recommendation.
prov
Groth, Paul and Moreau, Luc (2013). “PROV-Overview”. W3C, W3C Working Group Note.
rdf
Cyganiak, Richard, Wood, David, and Lanthaler, Markus (2014). “RDF 1.1 Concepts and Abstract Syntax”. W3C, W3C Recommendation.
rfc2046
Freed, Ned and Borenstein, Nathaniel S. (1996). “Multipurpose Internet Mail Extensions (MIME) Part Two: Media Types”. IETF, Request for Comments, RFC 2046.
rfc3987
Duerst, Martin and Suignard, Michel (2005). “Internationalized Resource Identifiers (IRIs)”. IETF, Request for Comments, RFC 3987.
rfc4122
Leach, Paul, Mealling, Michael, and Salz, Rich (2005). “A Universally Unique IDentifier (UUID) URN Namespace”. IETF, Request for Comments, RFC 4122.
rfc8141
Saint-Andre, Peter and Klensin, John (2017). “Uniform Resource Names (URNs)”. IETF, Request for Comments, RFC 8141.
rfc8785
Rundgren, Anders, Jordan, Bret, and Erdtman, Samuel (2020). “JSON Canonicalization Scheme (JCS)”. IETF, Request for Comments, RFC 8785.
rfc8949
Bormann, Carsten and Hoffman, Paul (2020). “Concise Binary Object Representation (CBOR)”. IETF, Request for Comments, RFC 8949.
rocksdb
Facebook Open Source. RocksDB: A persistent key-value store for fast storage.
Software
semantickernel
Microsoft (2023). Semantic Kernel.
spivak2012
Spivak, David I. (2012). “Functorial data migration”. Information and Computation, 217, pp. 31–51.
tikv
TiKV Authors. TiKV: A distributed transactional key-value database.
Software, Cloud Native Computing Foundation
trepplein
Ebner, Gabriel. trepplein: A type checker for Lean 3, written in Scala.
Software (historical reference for Lean 3)
trepplein4
Gadgil, Siddhartha. trepplein4: A type checker for Lean 4 export format.
Software
type_checking_in_lean4
Bailey, Chris. Type Checking in Lean 4.
Specification book
vercel-ai-sdk
Vercel. Vercel AI SDK.
Software
wasm-component-model
Bytecode Alliance (2023–2026). WebAssembly Component Model.
wasmtime
Bytecode Alliance. Wasmtime: A standalone runtime for WebAssembly.
Software
wit
Bytecode Alliance (2023–2026). WIT (WebAssembly Interface Type) Specification.
wit-bindgen
Bytecode Alliance (2023–2026). wit-bindgen: Component model bindings generator.
Software
xia2020
Xia, Li-yao, Zakowski, Yannick, He, Paul, Hur, Chung-Kil, Malecha, Gregory, Pierce, Benjamin C., and Zdancewic, Steve (2020). “Interaction trees: Representing recursive and impure programs in Coq”. Proceedings of the ACM on Programming Languages, 4(POPL).