Towards the theory of programming in constructive logic

DOI10.1007/3-540-52592-0_78MaRDI QIDQ4038676zbMATH OpenFDO

Authors Andrei Voronkov

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-52592-0_78

zbMATH Keywords

constructive logicconstructive semanticsenumerated modelsextracting programs from proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proofs and programs: A naïve approach to program extraction
• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 4187806
• Program development in constructive type theory
• scientific article; zbMATH DE number 4187141

Cited in

(27)

• A bridge between constructive logic and computer programming
• Program development in constructive type theory
• A theory of rules for enumerated classes of functions
• Extraction and verification of programs by analysis of formal proofs
• Program development in computational logic. A decade of research advances in logic-based program development.
• Writing constructive proofs yielding efficient extracted programs
• Extracting information from intermediate semiconstructive HA-systems -- extended abstract
• scientific article; zbMATH DE number 3850461 (Why is no real title available?)
• scientific article; zbMATH DE number 4143955 (Why is no real title available?)
• scientific article; zbMATH DE number 4145878 (Why is no real title available?)
• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 4148081 (Why is no real title available?)
• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• scientific article; zbMATH DE number 3907752 (Why is no real title available?)
• scientific article; zbMATH DE number 3952752 (Why is no real title available?)
• scientific article; zbMATH DE number 4057489 (Why is no real title available?)
• scientific article; zbMATH DE number 4089536 (Why is no real title available?)
• scientific article; zbMATH DE number 4093448 (Why is no real title available?)
• Provably recursive programs and program extraction
• On Uniformly Constructive and Semiconstructive Formal Systems
• Extracting non-deterministic concurrent programs
• Note on Conditional Constructivity
• scientific article; zbMATH DE number 4187141 (Why is no real title available?)
• scientific article; zbMATH DE number 4187806 (Why is no real title available?)
• Programming in equational logic: Beyond strong sequentiality
• The mathematical construction of a program

This page was built for publication: Towards the theory of programming in constructive logic

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