scientific article; zbMATH DE number 2003148
From MaRDI portal
Publication:4435458
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
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
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)