The paradox of trees in type theory

DOI10.1007/BF01995104MaRDI QIDQ688725zbMATH OpenFDO

Authors Thierry Coquand

Publication date 28 November 1993

Published in BIT (Search for Journal in Brave)

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

zbMATH Keywords

fixed-point operatorparadoxtype theory with \(W\)-types and a type of all types

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• On the structure of paradoxes
• scientific article; zbMATH DE number 1302061
• scientific article; zbMATH DE number 2185666
• A note on Russell's paradox in locally Cartesian closed categories
• scientific article; zbMATH DE number 733401

Cites work

• A construction of type: type in Martin-Löf's partial type theory with one universe
• Domain interpretations of Martin-Löf's partial type theory
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)

Cited in

(5)

• On the structure of paradoxes
• A short note on type-inhabitation: formula-trees vs. game semantics
• scientific article; zbMATH DE number 2185666 (Why is no real title available?)
• scientific article; zbMATH DE number 733401 (Why is no real title available?)
• A variation of Reynolds-Hurkens paradox

This page was built for publication: The paradox of trees in type theory

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