bibliography.bib

@book{norell2007towards,
  title={Towards a practical programming language based on dependent type theory},
  author={Norell, Ulf},
  volume={32},
  year={2007},
  publisher={Citeseer}
}

@inproceedings{de1972lambda,
  title={Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
  author={De Bruijn, Nicolaas Govert},
  booktitle={Indagationes Mathematicae (Proceedings)},
  volume={75},
  number={5},
  pages={381--392},
  year={1972},
  organization={Elsevier}
}

@InProceedings{auto,
  author="Kokke, Pepijn and Swierstra, Wouter",
  editor="Hinze, Ralf and Voigtl{\"a}nder, Janis",
  title="Auto in Agda",
  booktitle="Mathematics of Program Construction",
  year="2015",
  publisher="Springer International Publishing",
  address="Cham",
  pages="276--301",
  abstract="As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda's reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.",
}

@article{coinduction,
  Author = {Andreas Abel and James Chapman},
  Title = {Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types},
  Year = {2014},
  journal={arXiv preprint arXiv:1406.2059},
}

@InProceedings{mixfix,
  author="Danielsson, Nils Anders and Norell, Ulf",
  editor="Scholz, Sven-Bodo and Chitil, Olaf",
  title="Parsing Mixfix Operators",
  booktitle="Implementation and Application of Functional Languages",
  year="2011",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="80--99",
  abstract="A simple grammar scheme for expressions containing mixfix operators is presented. The scheme is parameterised by a precedence relation which is only restricted to be a directed acyclic graph; this makes it possible to build up precedence relations in a modular way. Efficient and simple implementations of parsers for languages with user-defined mixfix operators, based on the grammar scheme, are also discussed. In the future we plan to replace the support for mixfix operators in the language Agda with a grammar scheme and an implementation based on this work.",
}

@manual{agda-manual,
  title        = {Agda Language Reference},
  author       = {Ulf Norell and Andreas Abel and Nils Anders Danielsson and Makoto Takeyama and Catarina Coquand and Stevan Andjelkovic and Marcin Benke and Jean-Philippe Bernardy and James Chapman and Jesper Cockx and Dominique Devriese and Peter Divanski and Fredrik Nordvall Forsberg and Olle Fredriksson and Daniel Gustafsson and Philipp Hausmann and Patrik Jansson and Alan Jeffrey and Wolfram Kahl and Fredrik Lindblad and Francesco Mazzoli and Stefan Monnier and Darin Morrison and Guilhem Moulin and Nicolas Pouillard and Andrés Sicard-Ramírez and Andrea Vezzosi},
  year         = 2018,
  url          = {https://agda.readthedocs.io/en/v2.5.4.2/language/index.html},
  version      = {2.5.4.2}
}

@phdthesis{barras1997coq,
  title={The Coq proof assistant reference manual: Version 6.1},
  author={Barras, Bruno and Boutin, Samuel and Cornes, Cristina and Courant, Judica{\"e}l and Filliatre, Jean-Christophe and Gimenez, Eduardo and Herbelin, Hugo and Huet, Gerard and Munoz, Cesar and Murthy, Chetan and others},
  year={1997},
  school={Inria}
}

@article{landin1964mechanical,
  title={The mechanical evaluation of expressions},
  author={Landin, Peter J},
  journal={The Computer Journal},
  volume={6},
  number={4},
  pages={308--320},
  year={1964},
  publisher={The British Computer Society}
}

@article{landin1966next,
  title={The next 700 programming languages},
  author={Landin, Peter J},
  journal={Communications of the ACM},
  volume={9},
  number={3},
  pages={157--166},
  year={1966},
  publisher={ACM}
}

@inproceedings{danvy2004rational,
  title={A rational deconstruction of Landin’s SECD machine},
  author={Danvy, Olivier},
  booktitle={Symposium on Implementation and Application of Functional Languages},
  pages={52--71},
  year={2004},
  organization={Springer}
}

@misc{modernsecd,
  title={Functional programming languages, Part II: abstract machines},
  author={Xavier Leroy},
  year={2015--2016},
  url={https://xavierleroy.org/mpri/2-4/machines.pdf},
  howpublished={Course notes}
}

@misc{graham1989secd,
  title={Secd: Design issues},
  author={Graham, Brian},
  year={1989},
  publisher={University of Calgary}
}

@InProceedings{secdchip,
  author="Graham, Brian and Birtwistle, Graham",
  editor="Leeser, Miriam and Brown, Geoffrey",
  title="Formalising the design of an SECD chip", booktitle="Hardware Specification, Verification and Synthesis: Mathematical Aspects",
  year="1990",
  publisher="Springer New York",
  address="New York, NY",
  pages="40--66",
  abstract="We describe work completed on a custom SECD chip which is powerful enough to run a LispKit compiler. The 20,000 transistor design was fabricated in 1988 and is being interfaced to a workstation so that it can run downloaded programs. We discuss the evolution of the architecture from its abstract specification and abstraction issues that arose at key levels in the verification of the design. The verification is being undertaken in Cambridge HOL. One hard issue (garbage collection) has been left over for a second iteration of the specification and verification.",
}

@article{krivine2007call,
  title={A call-by-name lambda-calculus machine},
  author={Krivine, Jean-Louis},
  journal={Higher-order and symbolic computation},
  volume={20},
  number={3},
  pages={199--207},
  year={2007},
  publisher={Springer}
}

@phdthesis{leroy1990zinc,
  title={The ZINC experiment: an economical implementation of the ML language},
  author={Leroy, Xavier},
  year={1990},
  school={INRIA}
}

@book{friedman2018little,
  title={The Little Typer},
  author={Friedman, Daniel P and Christiansen, David Thrane},
  year={2018},
  publisher={MIT Press}
}

@book{stump2016verified,
  title={Verified functional programming in Agda},
  author={Stump, Aaron},
  year={2016},
  publisher={Morgan \& Claypool}
}

@inproceedings{mcbride2015turing,
  title={Turing-completeness totally free},
  author={McBride, Conor},
  booktitle={International Conference on Mathematics of Program Construction},
  pages={257--275},
  year={2015},
  organization={Springer}
}

@inproceedings{wadler2018programming,
  title={Programming Language Foundations in Agda},
  author={Wadler, Philip},
  booktitle={Brazilian Symposium on Formal Methods},
  pages={56--73},
  year={2018},
  organization={Springer}
}

@book{jacobs_2016,
  place={Cambridge},
  series={Cambridge Tracts in Theoretical Computer Science},
  title={Introduction to Coalgebra: Towards Mathematics of States and Observation},
  publisher={Cambridge University Press},
  author={Jacobs, Bart},
  year={2016},
  collection={Cambridge Tracts in Theoretical Computer Science}
}

@article{diaconescu1975axiom,
  title={Axiom of choice and complementation},
  author={Diaconescu, Radu},
  journal={Proceedings of the American Mathematical Society},
  volume={51},
  number={1},
  pages={176--178},
  year={1975}
}

@article{brouwer1907foundations,
  title={On the foundations of mathematics},
  author={Brouwer, Luitzen Egbertus Jan},
  journal={Collected works},
  volume={1},
  pages={11--101},
  year={1907},
  publisher={Citeseer}
}

@article{brouwer1908unreliability,
  title={LEJ Brouwer's ‘Unreliability of the Logical Principles’: A New Translation, with an Introduction},
  author={Van Atten, Mark and Sundholm, G{\"o}ran},
  journal={History and Philosophy of Logic},
  volume={38},
  number={1},
  pages={24--47},
  year={2017},
  publisher={Taylor \& Francis}
}

@InCollection{sep-logic-intuitionistic,
	author       =	{Moschovakis, Joan},
	title        =	{Intuitionistic Logic},
	booktitle    =	{The Stanford Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{https://plato.stanford.edu/archives/win2018/entries/logic-intuitionistic/}},
	year         =	{2018},
	edition      =	{Winter 2018},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}

@article{troelstra2011history,
  title={History of constructivism in the 20th century},
  author={Troelstra, Anne Sjerp},
  journal={Set Theory, Arithmetic, and Foundations of Mathematics},
  pages={150--179},
  year={2011},
  publisher={Cambridge University Press Cambridge}
}

@incollection{martin1975intuitionistic,
  title={An intuitionistic theory of types: Predicative part},
  author={Martin-L{\"o}f, Per},
  booktitle={Studies in Logic and the Foundations of Mathematics},
  volume={80},
  pages={73--118},
  year={1975},
  publisher={Elsevier}
}

@article{coquand2002formalised,
  title={A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions},
  author={Coquand, Catarina},
  journal={Higher-Order and Symbolic Computation},
  volume={15},
  number={1},
  pages={57--90},
  year={2002},
  publisher={Springer}
}

@misc{abel2013normalization,
  title={Normalization by Evaluation: Dependent Types and Impredicativity},
  author={Abel, Andreas},
  howpublished={Habilitationsschrift},
  year={2013}
}

@book{whitehead1912principia,
  title={Principia mathematica},
  author={Whitehead, Alfred North and Russell, Bertrand},
  volume={1},
  year={1910},
  publisher={University Press}
}

@incollection{frege1982philosophical,
  title={Correspondence with Frege},
  booktitle={Gottlob Frege: Philosophical and mathematical correspondence},
  author={Russell, Bertrand},
  note={Translated by Hans Kaal. Original from 1901.},
  publisher={University of Chicago Press},
  year={1982}
}

@incollection{von1923introduction,
  title={On the introduction of transfinite numbers},
  author={Von Neumann, John},
  booktitle={From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931},
  pages={346--354},
  year={2002},
  note={Translated by Jean van Heijenoort. Original from 1923.},
}

@article{church1940formulation,
  title={A formulation of the simple theory of types},
  author={Church, Alonzo},
  journal={The journal of symbolic logic},
  volume={5},
  number={2},
  pages={56--68},
  year={1940},
  publisher={Cambridge University Press}
}

@article{church1932set,
  title={A set of postulates for the foundation of logic},
  author={Church, Alonzo},
  journal={Annals of mathematics},
  pages={346--366},
  year={1932},
  publisher={JSTOR}
}

@article{kleene1935inconsistency,
  title={The inconsistency of certain formal logics},
  author={Kleene, Stephen C and Rosser, J Barkley},
  journal={Annals of Mathematics},
  pages={630--636},
  year={1935},
  publisher={JSTOR}
}

@article{turing1937computability,
  title={Computability and $\lambda$-definability},
  author={Turing, Alan M},
  journal={The Journal of Symbolic Logic},
  volume={2},
  number={4},
  pages={153--163},
  year={1937},
  publisher={Cambridge University Press}
}

@article{howard1980formulae,
  title={The formulae-as-types notion of construction},
  author={Howard, William A},
  journal={To HB Curry: essays on combinatory logic, lambda calculus and formalism},
  volume={44},
  pages={479--490},
  year={1980}
}

@article{gentzen1935untersuchungen,
  title={Untersuchungen {\"u}ber das logische Schlie{\ss}en. I},
  author={Gentzen, Gerhard},
  journal={Mathematische zeitschrift},
  volume={39},
  number={1},
  pages={176--210},
  year={1935},
  publisher={Springer}
}

@misc{de1967description,
  title={Description of the language Automath},
  author={de Bruijn, Nicolaas Govert},
  year={1967},
  publisher={Technische Hogeschool Eindhoven}
}

@inproceedings{voevodsky2011univalent,
  title={Univalent foundations of mathematics},
  author={Voevodsky, Vladimir},
  booktitle={International Workshop on Logic, Language, Information, and Computation},
  pages={4--4},
  year={2011},
  organization={Springer}
}

@book{nipkow2002isabelle,
  title={Isabelle/HOL: a proof assistant for higher-order logic},
  author={Nipkow, Tobias and Paulson, Lawrence C and Wenzel, Markus},
  volume={2283},
  year={2002},
  publisher={Springer Science \& Business Media}
}

@inproceedings{kaufmann1996acl2,
  title={ACL2: An industrial strength version of Nqthm},
  author={Kaufmann, Matt and Moore, J Strother},
  booktitle={Computer Assurance, 1996. COMPASS'96, Systems Integrity. Software Safety. Process Security. Proceedings of the Eleventh Annual Conference on},
  pages={23--34},
  year={1996},
  organization={IEEE}
}

@article{van2004lambda,
  title={A lambda calculus for quantum computation},
  author={Van Tonder, Andr{\'e}},
  journal={SIAM Journal on Computing},
  volume={33},
  number={5},
  pages={1109--1135},
  year={2004},
  publisher={SIAM}
}

@article{girard1987linear,
  title={Linear logic},
  author={Girard, Jean-Yves},
  journal={Theoretical computer science},
  volume={50},
  number={1},
  pages={1--101},
  year={1987},
  publisher={Elsevier}
}

@inproceedings{boudol1989towards,
  title={Towards a lambda-calculus for concurrent and communicating systems},
  author={Boudol, G{\'e}rard},
  booktitle={Colloquium on Trees in Algebra and Programming},
  pages={149--161},
  year={1989},
  organization={Springer}
}

@article{crandall19783,
  title={On the “3x+ 1” problem},
  author={Crandall, Richard E},
  journal={Mathematics of computation},
  volume={32},
  number={144},
  pages={1281--1292},
  year={1978}
}