Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68464OpenAlexW2484880499MaRDI QIDQ5477644FDOQ5477644

Authors Andrew M. Pitts

Publication date 6 July 2006

Full work available at URL https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• Alpha-structural recursion and induction
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Publication:4942633
• scientific article; zbMATH DE number 1222556
• Induction-recursion and initial algebras.
• scientific article; zbMATH DE number 2079043
• scientific article; zbMATH DE number 3857082
• Towards an algebraic theory of recursion
• Structures for structural recursion
• Recursion-theoretic hierarchies

Cited in

(3)

• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• Induction-recursion and initial algebras.
• Alpha-structural recursion and induction

This page was built for publication: Theorem Proving in Higher Order Logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5477644)