scientific article; zbMATH DE number 1552509

MaRDI QIDQ4524766zbMATH OpenFDO

Authors Holger Benl, Ulrich Berger, Helmut Schwichtenberg, Monika Seisenberger, Wolfgang Zuber

Publication date 29 July 2003

zbMATH Keywords

MINLOGsearch algorithm

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Minlog -- a tool for program extraction supporting algebras and coalgebras
• \textsc{Minlog}: a minimal logic theorem prover
• scientific article; zbMATH DE number 785043
• Program extraction from nested definitions
• Proofs and programs: A naïve approach to program extraction

Cited in

(19)

• Term rewriting for normalization by evaluation.
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Uniform Heyting arithmetic
• Axioms for strict and lazy functional programs
• Programs from proofs using classical dependent choice
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Extracting a DPLL algorithm
• On the constructive and computational content of abstract mathematics
• Unifying Sets and Programs via Dependent Types
• From Coinductive Proofs to Exact Real Arithmetic
• Intuitionistic completeness of first-order logic
• Unifying sets and programs via dependent types
• A realizability interpretation of Church's simple theory of types
• scientific article; zbMATH DE number 785043 (Why is no real title available?)
• Proof-theoretic notions for software maintenance
• \textsc{Minlog}: a minimal logic theorem prover
• Proofs, programs, processes
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• Types, Tableaus and Gödel’s God in Isabelle/HOL

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 Q4524766)