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

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

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Cited In (3)

• Induction-recursion and initial algebras.
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• 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)