scientific article; zbMATH DE number 1424052

zbMath0944.03008MaRDI QIDQ4945243

Jan Zwanenburg, Herman Geuvers, Erik Poll

Publication date: 7 June 2000

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

inductive typestyped \(\lambda\)-calculusfixed point combinatorhigher-order predicate logicbounded proof searchextension of type theoryunbounded proof search

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants

Uses Software

• Coq
• Automath