An operational approach to program extraction in the calculus of constructions

DOI10.1007/3-540-45013-0_10MaRDI QIDQ3079924zbMATH OpenOpenAlexFDO

Authors Maribel Fernández, Paula Severi

Publication date 4 March 2011

Published in Logic Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/20.500.12008/3482

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Studies of a theory of specifications with built-in program extraction
• Extraction of structured programs from specification proofs
• Proofs and programs: A naïve approach to program extraction
• Verifying programs in the calculus of inductive constructions
• Eliminating proofs from programs

Cited in

(6)

• Extraction of structured programs from specification proofs
• Controlling Program Extraction in Light Logics
• Extraction in Coq: An Overview
• Program extraction applied to monadic parsing
• Program extraction in exact real arithmetic
• Studies of a theory of specifications with built-in program extraction

This page was built for publication: An operational approach to program extraction in the calculus of constructions

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