An operational approach to program extraction in the calculus of constructions

DOI10.1007/3-540-45013-0_10zbMATH Open1278.68071OpenAlexW1529016461MaRDI QIDQ3079924FDOQ3079924

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

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

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)

Cited In (6)

• Extraction in Coq: An Overview
• Program extraction in exact real arithmetic
• Title not available (Why is that?)
• Controlling Program Extraction in Light Logics
• Studies of a theory of specifications with built-in program extraction
• Program extraction applied to monadic parsing

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)