dpndnt/library

Research library of the ##dependent IRC channel.

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

A

• A. Abel (2012) “Agda: Equality”
• A. Abel, S. Adelsberger, A. Setzer (2017) “Interactive programming in Agda: Objects and graphical user interfaces”
• A. Abel, J. Chapman (2014) “Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types”
• A. Abel, B. Pientka (2010) “Explicit substitutions for contextual type theory”
• S. Abramsky, A. Jung (1994) “Domain theory”
• P. Aczel (1977) “The type theoretic interpretation of constructive set theory”
• P. Aczel (1982) “The type theoretic interpretation of constructive set theory: Choice principles”
• G. Allais (2017) “Typing with leftovers: A mechanization of intuitionistic linear logic”
• N. Alechina, M. Mendler, V. de Paiva, E. Ritter (2001) “Categorical and Kripke semantics for constructive S4 modal logic”
• J. Alt, S. Artemov (2001) “Reflective λ-calculus”
• N. Amin, T. Rompf (2018) “Collapsing towers of interpreters”
• A. Appel (2001) “Foundational proof-carrying code”
• J. Armstrong (2003) “Making reliable distributed systems in the presence of software errors”
• J. Armstrong (2007) “A history of Erlang”
• S. Artemov (1999) “On explicit reflection in theorem proving and formal verification”
• S. Artemov (2001) “Explicit provability and constructive semantics”
• S. Artemov, E. Barzilay, R. Constable, A. Nogin (2001) “Reflection and propositions-as-types”
• S. Artemov, L. Beklemishev (2005) “Provability logic”
• S. Artemov, E. Bonelli (2007) “The intensional lambda calculus”
• S. Artemov, M. Fitting (2019) “Justification logic: Reasoning with reasons”
• S. Artemov, R. Iemhoff (2005) “The basic intuitionistic logic of proofs”
• R. Atkey, C. McBride (2013) “Productive coprogramming with guarded recursion”
• L. Augustsson (1985) “Compiling pattern matching”
• L. Augustsson (2006) “λ-calculus cooked four ways”

B

• R. Backhouse, P. Chisholm, G. Malcolm, E. Saaman (1989) “Do-it-yourself type theory”
• V. Balat, R. Di Cosmo, M. Fiore (2004) “Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums”
• D. Basin, S. Matthews, L. Viganò (1997) “Labelled propositional modal logics: Theory and practice”
• A. Bauer (2016) “On self-interpreters for Gödel’s System T”
• A. Bauer (2016) “On self-interpreters for System T and other typed λ-calculi”
• U. Berger, H. Schwichtenberg (1991) “An inverse of the evaluation functional for typed λ-calculus”
• J.-P. Bernardy, P. Jansson, R. Paterson (2010) “Parametricity and dependent types”
• G. Bierman, V. de Paiva (2000) “On an intuitionistic modal logic”
• E. Bishop (1973) “Schizophrenia in contemporary mathematics”
• E. Bishop (1975) “The crisis in contemporary mathematics”
• M. Boespflug, B. Pientka (2011) “Multi-level contextual type theory”
• E. Bonelli, F. Feller (2009) “The logic of proofs as a foundation for certifying mobile computation”
• M. Brown, J. Palsberg (2015) “Self-representation in Girard’s System U”
• M. Brown, J. Palsberg (2016) “Breaking through the normalization barrier: A self-interpreter for F-omega”
• M. Burrell, R. Cockett, B. Redmond (2009) “Pola: A language for PTIME programming”
• E. Burrows (2009) “A combinator processor”

C

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

D

• L. Damas, R. Milner (1982) “Principal type-schemes for functional programs”
• N. Danielsson (2012) “Operational semantics using the partiality monad”
• R. David, B. Guillaume (2001) “A λ-calculus with explicit weakening and explicit substitution”
• O. Danvy, M. Rhiger, K. Rose (2001) “Normalization by evaluation with typed abstract syntax”
• R. Davies (1996) “A temporal-logic approach to binding-time analysis”
• R. Davies, F. Pfenning (1996) “A modal analysis of staged computation”
• R. Davies, F. Pfenning (2001) “A modal analysis of staged computation”
• B. Delaware, B. Oliveira, T. Schrijvers (2013) “Meta-theory à la carte”
• J. Despeyroux, F. Pfenning, C. Schürmann (1997) “Primitive recursion for higher-order abstract syntax”
• D. Devriese, F. Piessens (2013) “Typed syntactic meta-programming”
• L. Diehl, D. Firsov, A. Stump (2018) “Generic zero-cost reuse for dependent types”
• L. Diehl (2017) “Fully generic programming over closed universes of inductive-recursive types”
• J. Dunfield, N. Krishnaswami (2019) “Bidirectional typing”
• P. Dybjer (1994) “Inductive families”
• P. Dybjer, A. Filinski (2002) “Normalization and partial evaluation”
• R. Dyckhoff (2015) “Some remarks on proof-theoretic semantics”
• R. Dyckhoff, L. Pinto (1997) “Proof search in constructive logics”

E

F

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

G

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

H

• T. Hagino (1987) “A categorical programming language”
• J.Y. Halpern, et al. (2001) “On the unusual effectiveness of logic in computer science”
• J. Harrison (1995) “Metatheory and reflection in theorem proving: A survey and critique”
• A. Heyting (1931) “The intuitionist foundations of mathematics”
• A. Heyting (1956) “Intuitionism: An introduction”
• C.A.R. Hoare, D.C.S. Allison (1972) “Incomputability”
• M. Hofmann (1997) “Extensional constructs in intensional type theory”

I

• R. Iemhoff (2001) “Provability logic and admissible rules”
• D. Ilik (2010) “Constructive completeness proofs and delimited control”
• D. Ilik (2013) “Continuation-passing style models complete for intuitionistic logic”

J

• R.P. James (2013) “The computational content of isomorphisms”
• E.T. Jaynes (1989) “Clearing up mysteries: The original goal”
• F. Joachimski, R. Matthes (2003) “Short proofs of normalization for the simply-typed λ-calculus, permutative conversions, and Gödel’s T”

K

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

L

• L. Lamport (1978) “Time, clocks, and the ordering of events in a distributed system”
• D. Leivant (1991) “Finely stratified polymorphism”
• C. Lewis, C. Langford (1932) “The structure of the system of strict implication”
• D.R. Licata, R. Harper (2010) “A monadic formalization of ML5”
• S. Lindley (2005) “Normalisation by evaluation in the compilation of typed functional programming languages”
• C. E. Linderholm (1971) “Mathematics Made Difficult”
• A. Löh, C. McBride, W. Swierstra (2010) “A tutorial implementation of a dependently typed lambda calculus”

M

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

N

• H. Nakano (2000) “A modality for recursion”
• H. Nakano (2001) “Fixed-point logic with the approximation modality and its Kripke completeness”
• A. Nanevski, F. Pfenning, B. Pientka (2007) “Contextual modal type theory”
• M. Naylor (2009) “Hardware-assisted and target-directed evaluation of functional programs”
• M. Naylor, C. Runciman (2008) “The Reduceron: Widening the von Neumann bottleneck for graph reduction using an FPGA”
• S. Negri (2005) “Proof analysis in modal logic”
• S. Negri (2011) “Proof theory for modal logic”
• E. Nogina (2014) “On logic of formal provability and explicit proofs”
• B. Nordstrom (1988) “Terminating general recursion”
• B. Nordstrom, K. Petersson, J. Smith (1990) “Programming in Martin-Löf’s type theory”
• A. Nuyts, A. Vezzosi, D. Devriese (2017) “Parametric quantifiers for dependent type theory”

O

• M. O’Neill (2008) “The genuine sieve of Eratosthenes”

P

• M. Parigot (1989) ”On the representation of data in lambda-calculus”
• L. Parreaux, A. Voizard, A. Shaikhha, C.E. Koch (2017) “Unifying analytic and statically-typed quasiquotes”
• A. Perlis (1982) “Epigrams on programming”
• F. Pfenning (2001) “Intensionality, extensionality, and proof irrelevance in modal type theory”
• F. Pfenning (2007) “On a logical foundation for explicit substitutions”
• F. Pfenning, R. Davies (2001) “A judgmental reconstruction of modal logic”
• F. Pfenning, P. Lee (1991) “Metacircularity in the polymorphic λ-calculus”
• B. Pientka (2007) “Functional programming with higher-order abstract syntax and explicit substitutions”
• D. Prawitz (1971) “Ideas and results in proof theory”
• H. Putnam (1980) “Models and reality”

Q

R

• T. Rendel, K. Ostermann, C. Hofer (2009) “Typed self-representation”
• J.C. Reynolds (1984) “Polymorphism is not set-theoretic”

S

• D. Sangiorgi (2009) “On the origins of bisimulation and coinduction”
• P. Schroeder-Heister (2010) “The categorical and the hypothetical: A critique of some fundamental assumptions of standard semantics”
• C. Schwaab, J.G. Siek (2013) “Modular type-safety proofs in Agda”
• J.P. Seldin, J.R. Hindley (1980) “To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism”
• C.E. Shannon (1948) “A mathematical theory of communication”
• T. Sheard (2001) “Accomplishments and research challenges in meta-programming”
• R. Simmons, B. Toninho (2011) “Constructive provability logic”
• A. Simpson (1994) “The proof theory and semantics of intuitionistic modal logic”
• P. Stansifer, M. Wand (2014) “Romeo: A system for more flexible binding-safe programming”
• G. Steren, E. Bonelli (2014) “Intuitionistic hypothetical logic of proofs”
• W.R. Stoye, T.J.W. Clarke, A.C. Norman (1984) “Some practical methods for rapid combinator reduction”
• T. Studer (2012) “Lectures on justification logic”
• A. Stump (2009) “Directly reflective meta-programming”
• W. Swierstra (2008) “Data types à la carte”

T

• W.W. Tait (1967) “Intensional interpretations of functionals of finite type I”
• A. Tarski (1936) “The concept of truth in formalized languages”
• K. Thompson (1984) “Reflections on trusting trust”
• W. Thurston (1994) “On proof and progress in mathematics”
• T. Toffoli (1980) “Reversible computing”
• D. Turner (1979) “A new implementation technique for applicative languages”
• D. Turner (2004) “Total functional programming”

U

V

• W. Veldman (1976) “An intuitionistic completeness theorem for intuitionistic predicate logic”
• V. Voevodsky (2014) “The origins and motivations of univalent foundations”

W

• P. Wadler (2015) “Propositions as types”
• P. van der Walt (2012) “Reflection in Agda”
• M. Wand (1998) “The theory of FEXPRs is trivial”
• M. Wand, D.P. Friedman (1986) “The mystery of the tower revealed: A non-reflective description of the reflective tower”
• B. Werner (1997) “Sets in types, types in sets”

X

Y

Z