imla2017
An Agda formalisation of a normalisation by evaluation procedure for the λ□-calculus, as composition of constructive soundness and completeness proofs for the necessity-only fragment of the intensional modal logic S4.
Part of my submission for the 7th Workshop on Intuitionistic Modal Logic and Applications (IMLA 2017), University of Toulouse, 17th to 28th July 2017.
References
-
Abel, A. (2013) “Normalization by evaluation: Dependent types and impredicativity”
-
Alechina, N., Mendler, M., de Paiva, V., Ritter, E. (2001) “Categorical and Kripke semantics for constructive S4 modal logic”
-
Altenkirch, T. (1993) “Proving strong normalization of CC by modifying realizability semantics”
-
Altenkirch, T., Reus, B. (1999) “Monadic presentations of lambda terms using generalized inductive types”
-
Artemov, S. N. (2001) “Explicit provability and constructive semantics”
-
Berger, U., Schwichtenberg, H. (1991) “An inverse of the evaluation functional for typed lambda-calculus”
-
Bierman, G. M., de Paiva, V. (2000) “On an intuitionistic modal logic”
-
Božić, M., Došen, K. (1984) “Models for normal intuitionistic modal logics”
-
Chapman, J. (2009) “Type checking and normalisation”
-
Coquand, C. (1993) “From semantics to rules: A machine assisted analysis”
-
Coquand, T., Dybjer, P. (1997) “Intuitionistic model constructions and normalization proofs”
-
Danvy, O. (1996) “Type-directed partial evaluation”
-
Dyckhoff, R. (2016) “Some remarks on proof-theoretic semantics”
-
Ewald, W. B. (1986) “Intuitionistic tense and modal logic”
-
Fischer Servi, G. (1984) “Axiomatizations for some intuitionistic modal logics”
-
Gabbay, M.J., Nanevski, A. (2012) “Denotation of contextual modal type theory: Syntax and meta-programming”
-
Girard, J.-Y., Taylor, P., Lafont, Y. (1989) “Proofs and types”
-
Gödel, K. (1933/1986) “Eine Interpretation des intuitionistischen Aussagenkalküls”
-
Iemhoff, R. (2001) “Provability logic and admissible rules”
-
Ilik, D. (2013) “Continuation-passing style models complete for intuitionistic logic”
-
Kripke, S. A. (1965) “Semantical analysis of intuitionistic logic I”
-
Martin-Löf, P. (1975) “An intuitionistic theory of types: Predicative part”
-
McCarthy, J., Abrahams, P. W., Edwards, D. J., Hart, T. P., Levin, M. I. (1962) “LISP 1.5 Programmer’s Manual”
-
McKinsey, J. C. C., Tarski, A. (1948) “Some theorems about the sentential calculi of Lewis and Heyting”
-
Nanevski, A., Pfenning, F., Pientka, B. (2008) “Contextual modal type theory”
-
Norell, U. (2007) “Towards a practical programming language based on dependent type theory”
-
Ono, H. (1977) “On some intuitionistic modal logics”
-
Pfenning, F., Davies, R. (2001) “A judgmental reconstruction of modal logic”
-
Plotkin, G. D., Stirling, C. (1986) “A framework for intuitionistic modal logics”
-
Sheard, T. (2001) “Accomplishments and research challenges in meta-programming”
-
Simpson, A. (1994) “The proof theory and semantics of intuitionistic modal logic”
-
Turner, D. A. (2004) “Total functional programming”
-
Wadler, P. (2015) “Propositions as types”
-
Wijesekera, D. (1990) “Constructive modal logics I”
About
Made by Miëtek Bak. Published under the MIT X11 license.