Program extraction in simply-typed higher order logic

DOI10.1007/3-540-39185-1_2MaRDI QIDQ4435458zbMATH OpenFDO

Authors Stefan Berghofer

Publication date 12 November 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2646/26460021.htm

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Types for Proofs and Programs
• Proofs and programs: A naïve approach to program extraction
• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 749923
• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics

Cited in

(30)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• \textsc{Prawf}: an interactive proof system for program extraction
• Intuitionistic fixed point logic
• Flyspeck II: The basic linear programs
• Proof terms for simply typed higher order logic
• Eliminating proofs from programs
• Proof-producing translation of higher-order logic into pure and stateful ML
• Extracting imperative programs from proofs: In-place Quicksort
• Controlling Program Extraction in Light Logics
• Program development by proof transformation.
• Extracting Purely Functional Contents from Logical Inductive Types
• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• Extraction of a program from deduction and its regularity. I
• An application of PER models to program extraction
• A formal framework for synthesis and verification of logic programs
• scientific article; zbMATH DE number 2079677 (Why is no real title available?)
• Deriving modular programs from short proofs
• A realizability interpretation of Church's simple theory of types
• First order marked types
• scientific article; zbMATH DE number 749923 (Why is no real title available?)
• On automating the extraction of programs from proofs using product types
• Program extraction applied to monadic parsing
• Types for Proofs and Programs
• Studies of a theory of specifications with built-in program extraction
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Program extraction from normalization proofs
• Proofs and programs: A naïve approach to program extraction
• A mechanized proof of the basic perturbation lemma
• Generating certified code from formal proofs: a case study in homological algebra

Describes a project that uses

Uses Software

• Isabelle/Isar
• Isabelle
• Isabelle/HOL
• HOL-OCL
• ETPS
• Nuprl

This page was built for publication: Program extraction in simply-typed higher order logic

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