Publication:3477935
From MaRDI portal
zbMath0699.68020MaRDI QIDQ3477935
Jean-Louis Krivine, Michel Parigot
Publication date: 1990
specifications; automatic programming; correct programs; mathematics as a programming language; second order intuitionistic
68Q60: Specification and verification (program logics, model checking, etc.)
68N01: General topics in the theory of software
03F35: Second- and higher-order arithmetic and fragments
Related Items
Proof normalization modulo, An ordinal measure based procedure for termination of functions, Completeness, minimal logic and programs extraction, The Girard-Reynolds isomorphism (second edition), Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation), Program development in constructive type theory, Recursive programming with proofs, Synthesis of ML programs in the system Coq, Classical logic, storage operators and second-order lambda-calculus, A general storage theorem for integers in call-by-name \(\lambda\)- calculus, Automatizing termination proofs of recursively defined functions, The Inf function in the system \(F\), A semantical storage operator theorem for all types, Additives of linear logic and normalization. I: A (restricted) Church-Rosser property., System ST toward a type system for extraction and proofs of programs, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, About classical logic and imperative programming, The Girard-Reynolds isomorphism, Controlling Program Extraction in Light Logics, Lambda-calcul, évaluation paresseuse et mise en mémoire
