An application of PER models to program extraction

DOI10.1017/S0960129500000244zbMath0797.68108OpenAlexW2142721976MaRDI QIDQ4282806

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

correctnesssemanticsprogram extractionspecificationtype theoryprogram synthesisprogram optimizationhigher order lambda calculusprograms from proofs

Mathematics Subject Classification ID

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

Related Items (1)

A simple model construction for the Calculus of Constructions

Uses Software

• Nuprl

Cites Work

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

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