Work in progress. Read the hyperlinked source.
See also the library of the ##dependent distributed research support group.
Made by Miëtek Bak. Licensed under CC BY-SA 4.0 .
- A. Abel (2013) Normalization by evaluation: Dependent types and impredicativity
- A. Abel, J. Chapman (2014) Normalization by evaluation in the delay monad
- 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
- T. Altenkirch (1993) Constructions, inductive types, and strong normalization
- S. Artemov (2001) Explicit provability and constructive semantics
- S. Artemov (2004) Kolmogorov and Gödel’s approach to intuitionistic logic: Current developments
- S. Artemov (2006) On two models of provability
- D. Basin, S. Matthews, L. Viganò (1997) Labelled propositional modal logics: Theory and practice
- G. Bierman, V. de Paiva (2000) On an intuitionistic modal logic
- J. Chapman (2008) Type checking and normalisation
- C. Coquand (1994) From semantics to rules: A machine assisted analysis
- T. Coquand, P. Dybjer (1997) Intuitionistic model constructions and normalization proofs
- R. Davies, F. Pfenning (2001) A modal analysis of staged computation
- L. Diehl, T. Sheard (2014) Hereditary substitution by canonical evaluation
- M.J. Gabbay, A. Nanevski (2012) Denotation of contextual modal type theory: Syntax and meta-programming
- Á. García-Pérez, P. Nogueira, J.J. Moreno Navarro (2013) Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order
- N. Ghani (1995) Adjoint rewriting
- R. Hakli, S. Negri (2010) Does the deduction theorem fail for modal logic?
- R. Iemhoff (2001) Provability logic and admissible rules
- D. Ilik (2010) Continuation-passing style models complete for intuitionistic logic
- F. Joachimski, R. Matthes (2003) Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and Gödel’s T
- C. Keller, T. Altenkirch (2010) Hereditary substitutions for simple types, formalized
- A. Kovacs (2017) A machine-checked correctness proof of NBE for STLC
- J. Malakhovski (2012) Reinventing formal logic
- M. Marti, T. Studer (2016) Intuitionistic modal logic made explicit
- C. McBride (2013) Dependently typed metaprogramming (in Agda)
- J.C. Mitchell (1996) Foundations for programming languages
- P. Morris (2007) Constructing universes for generic programming
- A. Nanevski, F. Pfenning, B. Pientka (2008) Contextual modal type theory
- H. Ono (1977) On some intuitionistic modal logics
- L. Paulson (1996) ML for the working programmer
- F. Pfenning, R. Davies (2001) A judgmental reconstruction of modal logic
- F. Pfenning (2010) Lecture notes on modal logic
- B. Pierce (2001) Types and programming languages
- S. Schäfer (2019) Engineering formal systems in constructive type theory
- P. Sestoft (2002) Demonstrating lambda calculus reduction
- A. Simpson (1994) The proof theory and semantics of intuitionistic modal logic
- G. Steren, E. Bonelli (2014) Intuitionistic hypothetical logic of proofs
- A. Stump (2016) Verified functional programming in Agda
- G. Winskel (1993) The formal semantics of programming languages