scientific article
From MaRDI portal
Publication:3477935
zbMath0699.68020MaRDI QIDQ3477935
Michel Parigot, Jean-Louis Krivine
Publication date: 1990
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
specificationsautomatic programmingcorrect programsmathematics as a programming languagesecond order intuitionistic
Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01) Second- and higher-order arithmetic and fragments (03F35)
Related Items (26)
Classical logic, storage operators and second-order lambda-calculus ⋮ A general storage theorem for integers in call-by-name \(\lambda\)- calculus ⋮ The Girard-Reynolds isomorphism ⋮ Automatizing termination proofs of recursively defined functions ⋮ The Inf function in the system \(F\) ⋮ Lambda-calcul, évaluation paresseuse et mise en mémoire ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ A semantical storage operator theorem for all types ⋮ Singleton, union and intersection types for program extraction ⋮ Machine Deduction ⋮ Additives of linear logic and normalization. I: A (restricted) Church-Rosser property. ⋮ System ST toward a type system for extraction and proofs of programs ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation) ⋮ Controlling Program Extraction in Light Logics ⋮ Program development in constructive type theory ⋮ Recursive programming with proofs ⋮ First order marked types ⋮ Genetic programming \(+\) proof search \(=\) automatic improvement ⋮ Proof normalization modulo ⋮ On automating the extraction of programs from proofs using product types ⋮ An ordinal measure based procedure for termination of functions ⋮ Completeness, minimal logic and programs extraction ⋮ About classical logic and imperative programming ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Synthesis of ML programs in the system Coq
This page was built for publication:
