Studies of a theory of specifications with built-in program extraction

DOI10.1023/A:1010663224299MaRDI QIDQ5951523zbMATH OpenOpenAlexFDO

Authors Paula Severi, Nora Szasz

Publication date 7 January 2002

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1010663224299

zbMATH Keywords

Martin-Löf's type theoryspecifications

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1617311
• Program Extraction in Constructive Analysis
• An operational approach to program extraction in the calculus of constructions
• scientific article; zbMATH DE number 2079677
• Refinement of classical proofs for program extraction
• scientific article; zbMATH DE number 2003148
• Extraction and verification of programs by analysis of formal proofs
• Refined program extraction from classical proofs: Some case studies
• Proofs and programs: A naïve approach to program extraction

Cited in

(9)

• System ST toward a type system for extraction and proofs of programs
• scientific article; zbMATH DE number 1617311 (Why is no real title available?)
• An operational approach to program extraction in the calculus of constructions
• scientific article; zbMATH DE number 3847387 (Why is no real title available?)
• scientific article; zbMATH DE number 4143955 (Why is no real title available?)
• scientific article; zbMATH DE number 4148081 (Why is no real title available?)
• An application of PER models to program extraction
• scientific article; zbMATH DE number 2079677 (Why is no real title available?)
• Propositions and specifications of programs in Martin-Löf's type theory

Describes a project that uses

Uses Software

• Automath
• ALF

This page was built for publication: Studies of a theory of specifications with built-in program extraction

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