Library of the ##dependent distributed research support group.
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. 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”
- 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”
- 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”
- 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”
- 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”
- 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”
- 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”
- 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”
- 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”
- 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. 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”
- 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”
- 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”
- R.S.S. O’Connor (2009) “Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory”
- M. O’Neill (2008) “The genuine sieve of Eratosthenes”
- 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”
- T. Rendel, K. Ostermann, C. Hofer (2009) “Typed self-representation”
- J.C. Reynolds (1984) “Polymorphism is not set-theoretic”
- 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”
- 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”
- W. Veldman (1976) “An intuitionistic completeness theorem for intuitionistic predicate logic”
- V. Voevodsky (2014) “The origins and motivations of univalent foundations”
- 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”