scientific article; zbMATH DE number 1161538

MaRDI QIDQ4393449zbMATH OpenFDO

Authors Hugo Johannes Elbers

Publication date 10 June 1998

zbMATH Keywords

\(\lambda\text{HOL}_\pi\)type theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Recommendations

• Some lambda calculus and type theory formalized
• Publication:4204148
• Mathematical Knowledge Management
• Faithfully reflecting the structure of informal mathematical proofs into formal type theories
• Type theory and formal proof. An introduction

Cited in

(4)

• Order-sorted inductive types
• Faithfully reflecting the structure of informal mathematical proofs into formal type theories
• scientific article; zbMATH DE number 1088190 (Why is no real title available?)
• Proof by computation in the Coq system

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