An application of PER models to program extraction

DOI10.1017/S0960129500000244MaRDI QIDQ4282806zbMATH OpenOpenAlexFDO

Authors Stefano Berardi

Publication date 14 March 1994

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129500000244

zbMATH Keywords

semanticsspecificationtype theoryprogram optimizationprogram extractioncorrectnessprogram synthesishigher order lambda calculusprograms from proofs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Metamathematics of constructive systems (03F50) Semantics in the theory of computing (68Q55)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 2003148
• Studies of a theory of specifications with built-in program extraction
• scientific article; zbMATH DE number 512774

Cites work

• Automatic synthesis of typed -programs on term algebras
• The calculus of constructions
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(2)

• scientific article; zbMATH DE number 2185653 (Why is no real title available?)
• A simple model construction for the calculus of constructions

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: An application of PER models to program extraction

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