Completeness, minimal logic and programs extraction

DOI10.1016/S0304-3975(99)00141-3MaRDI QIDQ5940922zbMATH OpenFDO

Authors Christophe Raffalli

Publication date 20 August 2001

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(99)00141-3

zbMATH Keywords

\(\lambda\)-calculus\(AF_2\)-type systemintuitionistic logicKripke semantics for minimal logicprogram extractiontypes

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
• Refinement of classical proofs for program extraction
• scientific article; zbMATH DE number 408816
• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 785043

Cites work

• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3111923 (Why is no real title available?)
• Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique

Cited in

(1)

• Controlling Program Extraction in Light Logics

This page was built for publication: Completeness, minimal logic and programs extraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5940922)