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) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Studies of a theory of specifications with built-in program extraction
• scientific article; zbMATH DE number 1617311
• 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)

• Studies of a theory of specifications with built-in program extraction
• Program extraction applied to monadic parsing
• Extraction in Coq: An Overview
• Program extraction in exact real arithmetic
• scientific article; zbMATH DE number 1617311 (Why is no real title available?)
• Controlling Program Extraction in Light Logics

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)