scientific article; zbMATH DE number 4187810
From MaRDI portal
zbMath0721.03048MaRDI QIDQ5752573
J. M. E. Hyland, Andrew M. Pitts
Publication date: 1989
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Grothendieck toposalgebraic toposesalgebraic-localic toposescategorical semantics of Martin-Löf's theory of dependent typesCoquand-Huet theory of constructionsuniversal types
Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Topoi (18B25) Second- and higher-order arithmetic and fragments (03F35)
Related Items
\(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
