An application of PER models to program extraction

DOI10.1017/S0960129500000244zbMATH Open0797.68108OpenAlexW2142721976MaRDI QIDQ4282806FDOQ4282806

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

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

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)

Cites Work

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

Cited In (2)

• Title not available (Why is that?)
• A simple model construction for the calculus of constructions

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)