Awesome

dpndnt/library

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

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

R.S.S. O’Connor (2009) “Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory”
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