scientific article; zbMATH DE number 1552510

MaRDI QIDQ4524768zbMATH OpenFDO

Authors Martin Strecker, Marko Luther, Friedrich W. von Henke

Publication date 15 January 2001

zbMATH Keywords

proof searchTYPELAB system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1614692
• scientific article; zbMATH DE number 65530
• Tactic theorem proving with refinement-tree proofs and metavariables
• Automated proof construction in type theory using resolution
• Tactics and parameters

Cited in

(6)

• scientific article; zbMATH DE number 1980941 (Why is no real title available?)
• Dependently Typed Programming Based on Automated Theorem Proving
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Tactic theorem proving with refinement-tree proofs and metavariables
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Tools and Algorithms for the Construction and Analysis of Systems

Describes a project that uses

Uses Software

• KIV
• ALF
• PVS

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