TheλμT-calculus
作者： Herman Geuvers , Robbert Krebbers , James McKinna
DOI: 10.1016/J.APAL.2012.05.005
关键词: Postponement 、 Simple type theory 、 Algebra 、 Computer science 、 Calculus 、 Mathematical proof 、 Natural number 、 Normalization (statistics) 、 Confluence
摘要: Abstract Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand operators, one should also include these in the calculus. As a first step that direction, we introduce λ μ T , combination Parigotʼs λμ-calculus and Godelʼs T, extend calculus datatype natural numbers primitive recursor. We consider problem confluence on raw terms, strong normalization for well-typed terms. Observing some problems extending proofs Baba et al. original proof, provide new, improved, (by complete developments) reducibility postponement argument) our system. conclude remarks about extensions, choices, prospects an improved presentation.
ru.nl
core.ac.uk
harvard.edu
arxiv.org
tue.nl
philpapers.org
ed.ac.uk
elsevier.com参考文章(35)
Ulrich Berger, Helmut Schwichtenberg, Program Development by Proof Transformation Springer, Berlin, Heidelberg. pp. 1- 45 ,(1995) , 10.1007/978-3-642-79361-5_1
Ken-etsu Fujita, Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value international conference on typed lambda calculi and applications. pp. 162- 177 ,(1999) , 10.1007/3-540-48959-2_13
Jean-Yves Girard, Paul Taylor, Yves Lafont, Proofs and types ,(1989)
Sören Stenlund, Combinators, λ-Terms and Proof Theory ,(2011)
Niels Jakob Rehof, Morten Heine Sørensen, The λΔ-calculus international symposium on theoretical aspects of computer software. pp. 516- 542 ,(1994) , 10.1007/3-540-57887-0_113
Michel Parigot, Classical Proofs as Programs KGC '93 Proceedings of the Third Kurt Gödel Colloquium on Computational Logic and Proof Theory. pp. 263- 276 ,(1993) , 10.1007/BFB0022575
Ken-etsu Fujita, Calculus of Classical Proofs I Lecture Notes in Computer Science. pp. 321- 335 ,(1997) , 10.1007/3-540-63875-X_62
Tristan Crolard, Emmanuel Polonowski, A program logic for higher-order procedural variables and non-local jumps arXiv: Logic in Computer Science. ,(2011)
René David, Karim Nour, Why the Usual Candidates of Reducibility Do Not Work for the Symmetric λμ-calculus Electronic Notes in Theoretical Computer Science. ,vol. 140, pp. 101- 111 ,(2005) , 10.1016/J.ENTCS.2005.06.020
Paweł Urzyczyn, Morten Heine Sørensen, Lectures on the Curry-Howard Isomorphism ,(2013)