Publication:3784072
From MaRDI portal
zbMath0643.03050MaRDI QIDQ3784072
Thomas Ehrhard, Thierry Coquand
Publication date: 1987
higher-order logic; fibration; indexed category; equational presentation; higher-order type system; polymorphic \(\lambda \)-calculus; semantics of F\(\omega \)
68Q60: Specification and verification (program logics, model checking, etc.)
03G30: Categorical logic, topoi
18D30: Fibered categories
03F35: Second- and higher-order arithmetic and fragments
03B40: Combinatory logic and lambda calculus
Related Items
E-ccc: between ccc and topos, - its expressive power from the viewpoint of data type theory, Alpha conversion, conditions on variables and categorical logic, Inheritance as implicit coercion, Categorical models of polymorphism, Categories of embeddings, Infinite hypergraphs. I: Basic properties, Domain theoretic models of polymorphism, Unnamed Item