research

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 .

References

• 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