scientific article; zbMATH DE number 2003148

zbMATH Open1023.68021MaRDI QIDQ4435458FDOQ4435458

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

Title of this publication is not available (Why is that?)

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

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)

Cited In (27)

• Flyspeck II: The basic linear programs
• A realizability interpretation of Church's simple theory of types
• Extracting Purely Functional Contents from Logical Inductive Types
• 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
• On automating the extraction of programs from proofs using product types
• Extracting imperative programs from proofs: In-place Quicksort
• Types for Proofs and Programs
• First order marked types
• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
• Title not available (Why is that?)
• Extraction of a program from deduction and its regularity. I
• A mechanized proof of the basic perturbation lemma
• Generating certified code from formal proofs: a case study in homological algebra
• Title not available (Why is that?)
• Eliminating proofs from programs
• Title not available (Why is that?)
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• Proofs and programs: A naïve approach to program extraction
• Controlling Program Extraction in Light Logics
• Proof-producing translation of higher-order logic into pure and stateful ML
• Intuitionistic fixed point logic
• Program development by proof transformation.
• Title not available (Why is that?)
• Program extraction from normalization proofs
• Studies of a theory of specifications with built-in program extraction
• Program extraction applied to monadic parsing

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)