library.bib

% ----------------------------------------------------------------------------
% A
%
% * A. Abel (2012) [“Agda: Equality”](doc/pdf/abel-2012.pdf)
% * A. Abel, S. Adelsberger, A. Setzer (2017) [“Interactive programming in Agda: Objects and graphical user interfaces”](doc/pdf/abel-adelsberger-setzer-2017.pdf)
% * A. Abel, J. Chapman (2014) [“Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types”](doc/pdf/abel-chapman-2014.pdf)
% * A. Abel, B. Pientka (2010) [“Explicit substitutions for contextual type theory”](doc/pdf/abel-pientka-2010.pdf)
% * S. Abramsky, A. Jung (1994) [“Domain theory”](doc/pdf/abramsky-jung-1994.pdf)
% * P. Aczel (1977) [“The type theoretic interpretation of constructive set theory”](doc/pdf/aczel-1977.pdf)
% * P. Aczel (1982) [“The type theoretic interpretation of constructive set theory: Choice principles”](doc/pdf/aczel-1982.pdf)
% * G. Allais (2017) [“Typing with leftovers: A mechanization of intuitionistic linear logic”](doc/pdf/allais-2017.pdf)
% * N. Alechina, M. Mendler, V. de Paiva, E. Ritter (2001) [“Categorical and Kripke semantics for constructive S4 modal logic”](doc/pdf/alechina-et-al-2001.pdf)
% * J. Alt, S. Artemov (2001) [“Reflective λ-calculus”](doc/pdf/alt-artemov-2001.pdf)
% * N. Amin, T. Rompf (2018) [“Collapsing towers of interpreters”](doc/pdf/amin-rompf-2018.pdf)
% * A. Appel (2001) [“Foundational proof-carrying code”](doc/pdf/appel-2001.pdf)
% * J. Armstrong (2003) [“Making reliable distributed systems in the presence of software errors”](doc/pdf/armstrong-2003.pdf)
% * J. Armstrong (2007) [“A history of Erlang”](doc/pdf/armstrong-2007.pdf)
% * S. Artemov (1999) [“On explicit reflection in theorem proving and formal verification”](doc/pdf/artemov-1999.pdf)
% * S. Artemov (2001) [“Explicit provability and constructive semantics”](doc/pdf/artemov-2001.pdf)
% * S. Artemov, E. Barzilay, R. Constable, A. Nogin (2001) [“Reflection and propositions-as-types”](doc/pdf/artemov-et-al-2001.pdf)
% * S. Artemov, L. Beklemishev (2005) [“Provability logic”](doc/pdf/artemov-beklemishev-2005.pdf)

@inproceedings{ArtemovBonelli2007,
  author    = {Sergei N.~Artemov and Eduardo Bonelli},
  year      = {2007},
  title     = {The intensional lambda calculus},
  editor    = {Sergei N.~Artemov and Anil Nerode},
  booktitle = {International Symposium on Logical Foundations of Computer Science (LFCS 2007), Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4514},
  pages     = {12--25},
  publisher = {Springer},
}

% * S. Artemov, M. Fitting (2019) [“Justification logic: Reasoning with reasons”](doc/pdf/artemov-fitting-2019.pdf)
% * S. Artemov, R. Iemhoff (2005) [“The basic intuitionistic logic of proofs”](doc/pdf/artemov-iemhoff-2005.pdf)
% * R. Atkey, C. McBride (2013) [“Productive coprogramming with guarded recursion”](doc/pdf/atkey-mcbride-2013.pdf)
% * L. Augustsson (1985) [“Compiling pattern matching”](doc/pdf/augustsson-1985.pdf)
% * L. Augustsson (2006) [“λ-calculus cooked four ways”](doc/pdf/augustsson-2006.pdf)


% ----------------------------------------------------------------------------
% B
%
% * R. Backhouse, P. Chisholm, G. Malcolm, E. Saaman (1989) [“Do-it-yourself type theory”](doc/pdf/backhouse-chisholm-malcolm-saaman-1989.pdf)
% * V. Balat, R. Di Cosmo, M. Fiore (2004) [“Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums”](doc/pdf/balat-dicosmo-fiore-2004.pdf)
% * D. Basin, S. Matthews, L. Viganò (1997) [“Labelled propositional modal logics: Theory and practice”](doc/pdf/basin-matthews-vigano-1997.pdf)

@inproceedings{Bauer2016a,
  author    = {Andrej Bauer},
  year      = {2016},
  title     = {On self-interpreters for {G}{\"o}del's {S}ystem {T}},
  editor    = {Silvia Ghelizan and Jelena Iveti{\'c}},
  booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016), Book of Abstracts},
  pages     = {23--24},
}

@misc{Bauer2016b,
  author    = {Andrej Bauer},
  year      = {2016},
  title     = {On self-interpreters for {S}ystem {T} and other typed $\lambda$-calculi},
  note      = {Available at \url{http://math.andrej.com/wp-content/uploads/2016/01/self-interpreter-for-T.pdf}},
}

% * U. Berger, H. Schwichtenberg (1991) [“An inverse of the evaluation functional for typed λ-calculus”](doc/pdf/berger-schwichtenberg-1991.pdf)
% * J.-P. Bernardy, P. Jansson, R. Paterson (2010) [“Parametricity and dependent types”](doc/pdf/bernardy-jansson-paterson-2010.pdf)
% * G. Bierman, V. de Paiva (2000) [“On an intuitionistic modal logic”](doc/pdf/bierman-depaiva-2000.pdf)
% * E. Bishop (1973) [“Schizophrenia in contemporary mathematics”](doc/pdf/bishop-1973.pdf)
% * E. Bishop (1975) [“The crisis in contemporary mathematics”](doc/pdf/bishop-1975.pdf)
% * M. Boespflug, B. Pientka (2011) [“Multi-level contextual type theory”](doc/pdf/boespflug-pientka-2011.pdf)
% * E. Bonelli, F. Feller (2009) [“The logic of proofs as a foundation for certifying mobile computation”](doc/pdf/bonelli-feller-2009.pdf)
% * M. Brown, J. Palsberg (2015) [“Self-representation in Girard’s System U”](doc/pdf/brown-palsberg-2015.pdf)

@inproceedings{BrownPalsberg2016,
  author    = {Matt Brown and Jens Palsberg},
  year      = {2016},
  title     = {Breaking through the normalization barrier: {A} self-interpreter for $\mathrm{F}_\omega$},
  editor    = {Rastislav Bod{\'{\i}}k and Rupak Majumdar},
  booktitle = {43rd Symposium on Principles of Programming Languages (POPL 2016), Proceedings},
  pages     = {5--17},
  publisher = {ACM},
}

% * M. Burrell, R. Cockett, B. Redmond (2009) [“Pola: A language for PTIME programming”](doc/pdf/burrell-cockett-redmond-2009.pdf)
% * E. Burrows (2009) [“A combinator processor”](doc/pdf/burrows-2009.pdf)


% ----------------------------------------------------------------------------
% C
%
% * J. Carette, C.-H. Chen, V. Choudhury, A. Sabry (2018) [“From reversible programs to univalent universes and back”](doc/pdf/carette-chen-choudhury-sabry-2018.pdf)
% * J. Carette, O. Kiselyov, C.-C. Shan (2009) [“Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages”](doc/pdf/carette-kiselyov-shan-2009.pdf)
% * J. Carette, A. Stump (2012) [“Towards typing for small-step direct reflection”](doc/pdf/carette-stump-2012.pdf)
% * J. Chapman (2009) [“Type checking and normalisation”](doc/pdf/chapman-2009.pdf)
% * J. Chapman, R. Kireev, C. Nester, P. Wadler (2019) [“System F in Agda, for fun and profit”](doc/pdf/chapman-kireev-nester-wadler-2019.pdf)
% * C.J. Cheney (1970) [“A nonrecursive list compacting algorithm”](doc/pdf/cheney-1970.pdf)
% * A. Chlipala (2008) [“Parametric higher-order abstract syntax for mechanized semantics”](doc/pdf/chlipala-2008.pdf)
% * D.R. Christiansen (2013) [“Bidirectional typing rules: A tutorial”](doc/pdf/christiansen-2013.pdf)
% * T.J.W. Clarke, P.J.S. Gladstone, C.D. MacLean, A.C. Norman (1980) [“SKIM: The S, K, I reduction machine”](doc/pdf/clarke-gladstone-maclean-norman-1980.pdf)
% * L. Convent, S. Lindley, C. McBride, C. McLaughlin (2020) [“Doo bee doo bee doo”](doc/pdf/convent-lindley-mcbride-mclaughlin-2020.pdf)
% * C. Coquand (2002) [“A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”](doc/pdf/coquand-2002.pdf)
% * T. Coquand (2004) [“About Brouwer’s fan theorem”](doc/pdf/coquand-2004.pdf)
% * T. Coquand, P. Dybjer (1994) [“Inductive definitions and type theory: An introduction (Preliminary version)”](doc/pdf/coquand-dybjer-1994.pdf)
% * T. Coquand, P. Dybjer (1997) [“Intuitionistic model constructions and normalization proofs”](doc/pdf/coquand-dybjer-1997.pdf)


% ----------------------------------------------------------------------------
% D
%
% * L. Damas, R. Milner (1982) [“Principal type-schemes for functional programs”](doc/pdf/damas-milner-1982.pdf)
% * N. Danielsson (2012) [“Operational semantics using the partiality monad”](doc/pdf/danielsson-2012.pdf)
% * R. David, B. Guillaume (2001) [“A λ-calculus with explicit weakening and explicit substitution”](doc/pdf/david-guillaume-2001.pdf)
% * O. Danvy, M. Rhiger, K. Rose (2001) [“Normalization by evaluation with typed abstract syntax”](doc/pdf/danvy-2001.pdf)
% * R. Davies (1996) [“A temporal-logic approach to binding-time analysis”](doc/pdf/davies-1996.pdf)

@inproceedings{DaviesPfenning1996,
  author    = {Rowan Davies and Frank Pfenning},
  year      = {1996},
  title     = {A modal analysis of staged computation},
  editor    = {Hans{-}Juergen Boehm and Guy L. Steele Jr.},
  booktitle = {23rd Symposium on Principles of Programming Languages (POPL 1996), Conference Record},
  pages     = {258--270},
  publisher = {ACM},
}

@article{DaviesPfenning2001,
  author    = {Rowan Davies and Frank Pfenning},
  year      = {2001},
  title     = {A modal analysis of staged computation},
  journal   = {Journal of the ACM},
  volume    = {48},
  number    = {3},
  pages     = {555--604},
}

% * B. Delaware, B. Oliveira, T. Schrijvers (2013) [“Meta-theory à la carte”](doc/pdf/delaware-oliveira-schrijvers-2013.pdf)
% * J. Despeyroux, F. Pfenning, C. Schürmann (1997) [“Primitive recursion for higher-order abstract syntax”](doc/pdf/despeyroux-pfenning-schurmann-1997.pdf)
% * D. Devriese, F. Piessens (2013) [“Typed syntactic meta-programming”](doc/pdf/devriese-piessens-2013.pdf)
% * L. Diehl, D. Firsov, A. Stump (2018) [“Generic zero-cost reuse for dependent types”](doc/pdf/diehl-firsov-stump-2018.pdf)
% * L. Diehl (2017) [“Fully generic programming over closed universes of inductive-recursive types”](doc/pdf/diehl-2017.pdf)
% * J. Dunfield, N. Krishnaswami (2019) [“Bidirectional typing”](doc/pdf/dunfield-krishnaswami-2019.pdf)
% * P. Dybjer (1994) [“Inductive families”](doc/pdf/dybjer-1994.pdf)
% * P. Dybjer, A. Filinski (2002) [“Normalization and partial evaluation”](doc/pdf/dybjer-filinski-2002.pdf)
% * R. Dyckhoff (2015) [“Some remarks on proof-theoretic semantics”](doc/pdf/dyckhoff-2015.pdf)
% * R. Dyckhoff, L. Pinto (1997) [“Proof search in constructive logics”](doc/pdf/dyckhoff-pinto-1997.pdf)


% ----------------------------------------------------------------------------
% E


% ----------------------------------------------------------------------------
% F
%
% * A. Filinski (1999) [“A semantic account of type-directed partial evaluation”](doc/pdf/filinski-1999.pdf)
% * A. Filinski (2001) [“Normalization by evaluation for the computational lambda-calculus”](doc/pdf/filinski-2001.pdf)
% * K. Foner (2015) [“Getting a quick fix on comonads”](doc/pdf/foner-2015.pdf)
% * N. Francez (2017) [“Does the implication elimination rule need a minor premise?”](doc/pdf/francez-2017.pdf)
% * E. Fredkin (2003) [“An introduction to digital philosophy”](doc/pdf/fredkin-2003.pdf)
% * E. Fredkin, T. Toffoli (1982) [“Conservative logic”](doc/pdf/fredkin-toffoli-1982.pdf)
% * E. Fredkin (1992) [“A new cosmogony”](doc/pdf/fredkin-1992.pdf)


% ----------------------------------------------------------------------------
% G
%
% * M. Gabbay, A. Nanevski (2012) [“Denotation of contextual modal type theory: Syntax and meta-programming”](doc/pdf/gabbay-nanevski-2012.pdf)
% * H. Geuvers (2001) [“Induction is not derivable in second order dependent type theory“](doc/pdf/geuvers-2001.pdf)
% * H. Geuvers (2009) [“Proof assistants: History, ideas and future”](doc/pdf/geuvers-2009.pdf)
% * J.-Y. Girard (1972) [“Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur”](doc/pdf/girard-1972.pdf)
% * L.C. González Huesca et al. (2020) [“Dual and axiomatic systems for constructive S4: A formally verified equivalence”](doc/pdf/gonzalez-huesca-et-al-2020.pdf)
% * K. Gödel (1933) [“An interpretation of the intuitionistic propositional calculus”](doc/pdf/godel-1933.pdf)
% * K. Gödel (1938) [“Lecture at Zilsel’s”](doc/pdf/godel-1938.pdf)


% ----------------------------------------------------------------------------
% H
%
% * T. Hagino (1987) [“A categorical programming language”](doc/pdf/hagino-1987.pdf)
% * J.Y. Halpern, et al. (2001) [“On the unusual effectiveness of logic in computer science”](doc/pdf/halpern-et-al-2001.pdf)
% * J. Harrison (1995) [“Metatheory and reflection in theorem proving: A survey and critique”](doc/pdf/harrison-1995.pdf)
% * A. Heyting (1931) [“The intuitionist foundations of mathematics”](doc/pdf/heyting-1931.pdf)
% * A. Heyting (1956) [“Intuitionism: An introduction”](doc/pdf/heyting-1956.pdf)

@article{HoareAllison1972,
  author    = {C.~A.~R.~Hoare and Donald C.~S.~Allison},
  year      = {1972},
  title     = {Incomputability},
  journal   = {ACM Computing Surveys},
  volume    = {4},
  number    = {3},
  pages     = {169--178},
}

% * M. Hofmann (1997) [“Extensional constructs in intensional type theory”](doc/pdf/hofmann-1997.pdf)


% ----------------------------------------------------------------------------
% I
%
% * R. Iemhoff (2001) [“Provability logic and admissible rules”](doc/pdf/iemhoff-2001.pdf)
% * D. Ilik (2010) [“Constructive completeness proofs and delimited control”](doc/pdf/ilik-2010.pdf)
% * D. Ilik (2013) [“Continuation-passing style models complete for intuitionistic logic”](doc/pdf/ilik-2013.pdf)


% ----------------------------------------------------------------------------
% J
%
% * R.P. James (2013) [“The computational content of isomorphisms”](doc/pdf/james-2013.pdf)
% * E.T. Jaynes (1989) [“Clearing up mysteries: The original goal”](doc/pdf/jaynes-1989.pdf)
% * F. Joachimski, R. Matthes (2003) [“Short proofs of normalization for the simply-typed λ-calculus, permutative conversions, and Gödel’s T”](doc/pdf/joachimski-matthes-2002.pdf)


% ----------------------------------------------------------------------------
% K
%
% * P.A. Karger, R.R. Schell (1974) [“Multics security evaluation: Vulnerability analysis”](doc/pdf/karger-schell-1974.pdf)
% * C. Keller, T. Altenkirch (2010) [“Hereditary substitutions for simple types, formalized”](doc/pdf/keller-altenkirch-2010.pdf)
% * D. Kesner (2007) [“The theory of calculi with explicit substitutions revisited”](doc/pdf/kesner-2007.pdf)
% * I.-S. Kim, K. Yi, C. Calcagno (2006) [“A polymorphic modal type system for Lisp-like multi-staged languages”](doc/pdf/kim-yi-calcagno-2006.pdf)
% * A. Kovács (2017) [“A machine-checked correctness proof of normalization by evaluation for simply typed lambda calculus”](doc/pdf/kovacs-2017.pdf)
% * S. Kripke (1963) [“Semantical analysis of modal logic I: Normal modal logic propositional calculi”](doc/pdf/kripke-1963.pdf)


% ----------------------------------------------------------------------------
% L
%
% * L. Lamport (1978) [“Time, clocks, and the ordering of events in a distributed system”](doc/pdf/lamport-1978.pdf)
% * D. Leivant (1991) [“Finely stratified polymorphism”](doc/pdf/leivant-1991.pdf)
% * C. Lewis, C. Langford (1932) [“The structure of the system of strict implication”](doc/pdf/lewis-langford-1932.pdf)
% * D.R. Licata, R. Harper (2010) [“A monadic formalization of ML5”](doc/pdf/licata-harper-2010.pdf)
@book{linderholm_1971,
      title={Mathematics made difficult},
      publisher={New York, World Pub},
      author={Linderholm, Carle E},
      year={1971}
}
% * S. Lindley (2005) [“Normalisation by evaluation in the compilation of typed functional programming languages”](doc/pdf/lindley-2005.pdf)
% * A. Löh, C. McBride, W. Swierstra (2010) [“A tutorial implementation of a dependently typed lambda calculus”](doc/pdf/loh-mcbride-swierstra-2010.pdf)


% ----------------------------------------------------------------------------
% M
%
% * D. McAdams (2013) [“A tutorial on the Curry-Howard correspondence”](doc/pdf/mcadams-2013.pdf)
% * C. McBride (1999) [“Dependently typed functional programs and their proofs”](doc/pdf/mcbride-1999.pdf)
% * C. McBride (2003) [“First-order unification by structural recursion”](doc/pdf/mcbride-2003.pdf)
% * C. McBride (2009) [“Let’s see how things unfold: Reconciling the infinite with the intensional”](doc/pdf/mcbride-2009.pdf)
% * C. McBride (2015) [“Turing-completeness totally free”](doc/pdf/mcbride-2015.pdf)
% * C. McBride (2016) [“I got plenty o’ nuttin’”](doc/pdf/mcbride-2016.pdf)
% * G.H. Mealy (1955) [“A method for synthesizing sequential circuits”](doc/pdf/mealy-1955.pdf)
% * P.-A. Mellies (1995) [“Typed λ-calculi with explicit substitutions may not terminate”](doc/pdf/mellies-1995.pdf)
% * P.F. Mendler (1987) [“Inductive definition in type theory”](doc/pdf/mendler-1987.pdf)
% * D.B. Miller, E. Fredkin (2005) [“Two-state, reversible, universal cellular automata in three dimensions”](doc/pdf/miller-fredkin-2005.pdf)
% * A. Miquel (2001) [”The implicit calculus of constructions”](doc/pdf/miquel-2001.pdf)
% * E. Moggi (1989) [“Computational lambda-calculus and monads”](doc/pdf/moggi-1989.pdf)
% * E. Moggi (1991) [“Notions of computation and monads”](doc/pdf/moggi-1991.pdf)
% * P. Morris (2007) [“Constructing universes for generic programming”](doc/pdf/morris-2007.pdf)


% ----------------------------------------------------------------------------
% N
%
% * H. Nakano (2000) [“A modality for recursion”](doc/pdf/nakano-2000.pdf)
% * H. Nakano (2001) [“Fixed-point logic with the approximation modality and its Kripke completeness”](doc/pdf/nakano-2001.pdf)

@article{NanevskiPfenningPientka2008,
  author    = {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka},
  year      = {2008},
  title     = {Contextual modal type theory},
  journal   = {ACM Transactions on Computational Logic},
  volume    = {9},
  number    = {3},
  pages     = {1--49},
}

% * M. Naylor (2009) [“Hardware-assisted and target-directed evaluation of functional programs”](doc/pdf/naylor-2009.pdf)
% * M. Naylor, C. Runciman (2008) [“The Reduceron: Widening the von Neumann bottleneck for graph reduction using an FPGA”](doc/pdf/naylor-runciman-2008.pdf)
% * S. Negri (2005) [“Proof analysis in modal logic”](doc/pdf/negri-2005.pdf)
% * S. Negri (2011) [“Proof theory for modal logic”](doc/pdf/negri-2011.pdf)
% * E. Nogina (2014) [“On logic of formal provability and explicit proofs”](doc/pdf/nogina-2014.pdf)
% * B. Nordstrom (1988) [“Terminating general recursion”](doc/pdf/nordstrom-1988.pdf)
% * B. Nordstrom, K. Petersson, J. Smith (1990) [“Programming in Martin-Löf’s type theory”](doc/pdf/nordstrom-petersson-smith-1990.pdf)
% * A. Nuyts, A. Vezzosi, D. Devriese (2017) [“Parametric quantifiers for dependent type theory”](doc/pdf/nuyts-vezzosi-devriese-2017.pdf)


% ----------------------------------------------------------------------------
% O
%

@book{OConnor2009,
  title={Incompleteness \& Completeness: Formalizing Logic and Analysis in Type Theory},
  author={O'Connor, R.S.S.},
  isbn={9789090244556},
  series={IPA dissertation series},
  url={https://hdl.handle.net/2066/76032},
  year={2009}
}

% * M. O’Neill (2008) [“The genuine sieve of Eratosthenes”](doc/pdf/oneill-2008.pdf)


% ----------------------------------------------------------------------------
% P
%
% * M. Parigot (1989) [”On the representation of data in lambda-calculus”](doc/pdf/parigot-1989.pdf)
% * L. Parreaux, A. Voizard, A. Shaikhha, C.E. Koch (2017) [“Unifying analytic and statically-typed quasiquotes”](doc/pdf/parreaux-voizard-shaikhha-koch-2017.pdf)
% * A. Perlis (1982) [“Epigrams on programming”](doc/pdf/perlis-1982.pdf)
% * F. Pfenning (2001) [“Intensionality, extensionality, and proof irrelevance in modal type theory”](doc/pdf/pfenning-2001.pdf)
% * F. Pfenning (2007) [“On a logical foundation for explicit substitutions”](doc/pdf/pfenning-2007.pdf)

@article{PfenningDavies2001,
  author    = {Frank Pfenning and Rowan Davies},
  year      = {2001},
  title     = {A judgmental reconstruction of modal logic},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {11},
  number    = {4},
  pages     = {511--540},
}

% * F. Pfenning, P. Lee (1991) [“Metacircularity in the polymorphic λ-calculus”](doc/pdf/pfenning-lee-1991.pdf)
% * B. Pientka (2007) [“Functional programming with higher-order abstract syntax and explicit substitutions”](doc/pdf/pientka-2007.pdf)
% * D. Prawitz (1971) [“Ideas and results in proof theory”](doc/pdf/prawitz-1971.pdf)
% * H. Putnam (1980) [“Models and reality”](doc/pdf/putnam-1980.pdf)


% ----------------------------------------------------------------------------
% Q
%


% ----------------------------------------------------------------------------
% R
%
% * T. Rendel, K. Ostermann, C. Hofer (2009) [“Typed self-representation”](doc/pdf/rendel-ostermann-hofer-2009.pdf)
% * J.C. Reynolds (1984) [“Polymorphism is not set-theoretic”](doc/pdf/reynolds-1984.pdf)


% ----------------------------------------------------------------------------
% S
%
% * D. Sangiorgi (2009) [“On the origins of bisimulation and coinduction”](doc/pdf/sangiorgi-2009.pdf)
% * P. Schroeder-Heister (2010) [“The categorical and the hypothetical: A critique of some fundamental assumptions of standard semantics”](doc/pdf/schroederheister-2010.pdf)
% * C. Schwaab, J.G. Siek (2013) [“Modular type-safety proofs in Agda”](doc/pdf/schwaab-siek-2013.pdf)
% * J.P. Seldin, J.R. Hindley (1980) [“To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism”](doc/pdf/seldin-hindley-1980.pdf)
% * C.E. Shannon (1948) [“A mathematical theory of communication”](doc/pdf/shannon-1948.pdf)

@inproceedings{Sheard2001,
  author    = {Tim Sheard},
  year      = {2001},
  title     = {Accomplishments and research challenges in meta-programming},
  booktitle = {2nd International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG 2001), Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2196},
  pages     = {2--44},
  publisher = {Springer},
}

% * R. Simmons, B. Toninho (2011) [“Constructive provability logic”](doc/pdf/simmons-toninho-2011.pdf)
% * A. Simpson (1994) [“The proof theory and semantics of intuitionistic modal logic”](doc/pdf/simpson-1994.pdf)
% * P. Stansifer, M. Wand (2014) [“Romeo: A system for more flexible binding-safe programming”](doc/pdf/stansifer-wand-2014.pdf)
% * G. Steren, E. Bonelli (2014) [“Intuitionistic hypothetical logic of proofs”](doc/pdf/steren-bonelli-2014.pdf)
% * W.R. Stoye, T.J.W. Clarke, A.C. Norman (1984) [“Some practical methods for rapid combinator reduction”](doc/pdf/stoye-clarke-norman-1984.pdf)
% * T. Studer (2012) [“Lectures on justification logic”](doc/pdf/studer-2012.pdf)
% * A. Stump (2009) [“Directly reflective meta-programming”](doc/pdf/stump-2009.pdf)
% * W. Swierstra (2008) [“Data types à la carte”](doc/pdf/swierstra-2008.pdf)


% ----------------------------------------------------------------------------
% T
%
% * W.W. Tait (1967) [“Intensional interpretations of functionals of finite type I”](doc/pdf/tait-1967.pdf)
% * A. Tarski (1936) [“The concept of truth in formalized languages”](doc/pdf/tarski-1936.pdf)
% * K. Thompson (1984) [“Reflections on trusting trust”](doc/pdf/thompson-1984.pdf)
% * W. Thurston (1994) [“On proof and progress in mathematics”](doc/pdf/thurston-1994.pdf)
% * T. Toffoli (1980) [“Reversible computing”](doc/pdf/toffoli-1980.pdf)
% * D. Turner (1979) [“A new implementation technique for applicative languages”](doc/pdf/turner-1979.pdf)
% * D. Turner (2004) [“Total functional programming”](doc/pdf/turner-2004.pdf)


% ----------------------------------------------------------------------------
% U
%


% ----------------------------------------------------------------------------
% V
%
% * W. Veldman (1976) [“An intuitionistic completeness theorem for intuitionistic predicate logic”](doc/pdf/veldman-1976.pdf)
% * V. Voevodsky (2014) [“The origins and motivations of univalent foundations”](doc/pdf/voevodsky-2014.pdf)


% ----------------------------------------------------------------------------
% W
%
% * P. Wadler (2015) [“Propositions as types”](doc/pdf/wadler-2015.pdf)
% * P. van der Walt (2012) [“Reflection in Agda”](doc/pdf/vanderwalt-2012.pdf)
% * M. Wand (1998) [“The theory of FEXPRs is trivial”](doc/pdf/wand-1998.pdf)
% * M. Wand, D.P. Friedman (1986) [“The mystery of the tower revealed: A non-reflective description of the reflective tower”](doc/pdf/wand-friedman-1986.pdf)
% * B. Werner (1997) [“Sets in types, types in sets”](doc/pdf/werner-1997.pdf)


% ----------------------------------------------------------------------------
% X
%


% ----------------------------------------------------------------------------
% Y
%


% ----------------------------------------------------------------------------
% Z
%