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: 71.
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.
artemov-fitting2019
Artemov, Sergei and Fitting, Melvin (2019). Justification Logic: Reasoning with Reasons. Cambridge Tracts in Mathematics, Cambridge University Press.
The monograph D39 and D73 build on. Copy under references/publications/. Its copyright page reads “First published 2019”; some design docs cite it as 2020
artemov1995
Artemov, Sergei (1995). “Operational modal logic”. Mathematical Sciences Institute, Cornell University, MSI 95-29.
Introduces the Logic of Proofs (LP) — the first internalisation of evidence terms into the object language
artemov2008
Artemov, Sergei (2008). “The Logic of Justification”. The Review of Symbolic Logic, 1(4), pp. 477–513.
DOI: 10.1017/S1755020308090060
atomicdata
Meindertsma, Joep (2020–2026). Atomic Data: A modular specification for sharing, modifying and modeling graph data.
W3C Community Group Specification
baldridge2002
Baldridge, Jason (2002). Lexically Specified Derivational Control in Combinatory Categorial Grammar. PhD thesis, University of Edinburgh.
The multimodal slashes
lexicon:Mode' mirrors: the modality hierarchy that lets a determiner benp/$\diamond$n’ while a permutative functor is not
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)
chan2019wrn
Chan, Edmond M., Shibue, Tsukasa, McFarland, James M., Gaeta, Benjamin, Ghandi, Mahmoud, Dumont, Nancy, Gonzalez, Alfredo, McPartlan, Justine S., Li, Tianxia, Zhang, Yanxi, Liu, Jie Bin, Lazaro, Jean-Bernard, Gu, Peili, Piett, Cortt G., Apffel, Annie, Ali, Siraj M., Deasy, Rebecca, Keskula, Paula, Ng, Raymond W. S., Roberts, Justine, Reddy, Alanna, Cowley, Glenn S., Stegmaier, Kimberly, Hahn, William C., Root, David E., Boehm, Jesse S., and Vazquez, Francisca (2019). “WRN helicase is a synthetic lethal target in microsatellite unstable cancers”. Nature, 568, pp. 551–556.
DOI: 10.1038/s41586-019-1102-x
The paper demo/prose-to-formulas and experiments/publications/wrn-helicase formalise
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).
eisner1996
Eisner, Jason (1996). “Efficient Normal-Form Parsing for Combinatory Categorial Grammar”. In Proceedings of the 34th Annual Meeting of the Association for Computational Linguistics (ACL), pp. 79–86.
Normal-form constraints on spurious ambiguity — the problem `dcg::chart’ packs against
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.
huddleston-pullum2002
Huddleston, Rodney and Pullum, Geoffrey K. (2002). The Cambridge Grammar of the English Language. Cambridge University Press.
The descriptive reference behind the closed-class inventory and the D62 category features
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.
goldberg1991
Goldberg, David (1991). “What every computer scientist should know about floating-point arithmetic”. ACM Computing Surveys 23(1), 5–48.
Cited by D86 §3.4 for the decision to admit IEEE NaN with its defined behaviour rather than refine it away.
ltn
Badreddine, Samy, Garcez, Artur d’Avila, Serafini, Luciano, and Spranger, Michael (2022). “Logic tensor networks”. Artificial Intelligence, 303.
mclean-horspool1996
McLean, Philippe and Horspool, R. Nigel (1996). “A Faster Earley Parser”. In Compiler Construction (CC ‘96), Lecture Notes in Computer Science 1060, pp. 281–293, Springer.
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.
miller1991
Miller, Dale (1991). “A logic programming language with lambda-abstraction, function variables, and simple unification”. Journal of Logic and Computation, 1(4), pp. 497–536.
The “Miller fragment” — each free variable applied to distinct bound variables, no projections
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.
steedman2000
Steedman, Mark (2000). The Syntactic Process. MIT Press.
The CCG lineage `lexicon:Cat’ follows
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).