A program logic for higher-order procedural variables and non-local jumps
作者： Tristan Crolard , Emmanuel Polonowski
DOI:
关键词:
摘要: Relying on the formulae-as-types paradigm for classical logic, we define a program logic an imperative language with higher-order procedural variables and non-local jumps. Then, show how to derive sound this programming language. As by-product, obtain non-dependent type system which is more permissive than what usually found in statically typed languages. generic example, encode versions of delimited continuations operators shift reset.
arxiv.org
harvard.edu参考文章(73)
Harvey Friedman, Classically and intuitionistically provably recursive functions Springer Berlin Heidelberg. pp. 21- 27 ,(1978) , 10.1007/BFB0103100
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
Sigekatu Kuroda, Intuitionistische Untersuchungen der formalistischen Logik Nagoya Mathematical Journal. ,vol. 2, pp. 35- 47 ,(1951) , 10.1017/S0027763000010023
Hayo Thielecke, An Introduction to Landin‘s “A Generalization of Jumps and Labels” Higher-Order and Symbolic Computation archive. ,vol. 11, pp. 117- 123 ,(1998) , 10.1023/A:1010060315625
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
Bernhard Reus, Thomas Streicher, About hoare logics for higher-order store international colloquium on automata languages and programming. pp. 1337- 1348 ,(2005) , 10.1007/11523468_108
Iman Poernomo, Proofs-as-Imperative-Programs: Application to Synthesis of Contracts international andrei ershov memorial conference on perspectives of system informatics. pp. 112- 119 ,(2003) , 10.1007/978-3-540-39866-0_13
Von Kurt Gödel, ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES Dialectica. ,vol. 12, pp. 280- 287 ,(1958) , 10.1111/J.1746-8361.1958.TB01464.X
Daniel Leivant, Contracting proofs to programs ,(1989)
Peter J. Landin, A Generalization of Jumps and Labels Higher-Order and Symbolic Computation archive. ,vol. 11, pp. 125- 143 ,(1998) , 10.1023/A:1010068630801