scientific article; zbMATH DE number 2185666

MaRDI QIDQ3024841zbMATH OpenFDO

Authors Antonius J. C. Hurkens

Publication date 4 July 2005

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 733401
• scientific article; zbMATH DE number 226803
• The paradox of trees in type theory
• On the structure of paradoxes
• A construction of type: type in Martin-Löf's partial type theory with one universe

Cited in

(18)

• On paradoxes in normal form
• scientific article; zbMATH DE number 988702 (Why is no real title available?)
• Deconstruct the Graham’s Paradox
• In the Search of a Naive Type Theory
• Polymorphism and the obstinate circularity of second order logic: a victims' tale
• Cumulative inductive types in Coq
• An extended type system with lambda-typed lambda-expressions
• Interactive programming in Agda -- objects and graphical user interfaces
• A modular construction of type theories
• A New Foundational Crisis in Mathematics, Is It Really Happening?
• Is Impredicativity Implicitly Implicit
• Paradoxes, intuitionism, and proof-theoretic semantics
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
• Covering spaces in homotopy type theory
• The rewster: type preserving rewrite rules for the Coq proof assistant
• The paradox of trees in type theory
• A variation of Reynolds-Hurkens paradox
• The Rewster: type preserving rewrite rules for the Rocq Prover. Extended version of the ITP 2024 paper

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