scientific article; zbMATH DE number 2003148

MaRDI QIDQ4435458zbMATH OpenFDO

Authors Stefan Berghofer

Publication date 12 November 2003

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

Mathematics Subject Classification ID

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

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

(27)

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

Describes a project that uses

Uses Software

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

This page was built for publication:

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