scientific article; zbMATH DE number 4187810

zbMath0721.03048MaRDI QIDQ5752573

J. M. E. Hyland, Andrew M. Pitts

Publication date: 1989

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Grothendieck toposalgebraic toposesalgebraic-localic toposescategorical semantics of Martin-Löf's theory of dependent typesCoquand-Huet theory of constructionsuniversal types

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Topoi (18B25) Second- and higher-order arithmetic and fragments (03F35)

Related Items (31)

\(F\)-semantics for type assignment systems ⋮ Term graph rewriting and garbage collection using opfibrations ⋮ On completeness and cocompleteness in and around small categories ⋮ A higher-order calculus and theory abstraction ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ A category-theoretic account of program modules ⋮ Quantitative domains, groupoids and linear logic ⋮ Dictoses ⋮ Semantics for abstract clauses ⋮ An exper model for Quest ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ A note on Russell's paradox in locally Cartesian closed categories ⋮ A modest model of records, inheritance, and bounded quantification ⋮ Inheritance as implicit coercion ⋮ Type checking with universes ⋮ The extended calculus of constructions (ECC) with inductive types ⋮ A simple model construction for the Calculus of Constructions ⋮ Constructing type systems over an operational semantics ⋮ Aspects of predicative algebraic set theory. I: Exact completion ⋮ Combinatorial structure of type dependency ⋮ Comprehension categories and the semantics of type dependency ⋮ On the semantics of classical disjunction ⋮ Unnamed Item ⋮ Unnamed Item ⋮ From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality ⋮ A constructive theory of continuous domains suitable for implementation ⋮ Notions of computation and monads ⋮ From term models to domains ⋮ Unnamed Item ⋮ Equilogical spaces ⋮ A natural semantics of first-order type dependency

This page was built for publication: