scientific article
From MaRDI portal
Publication:3786612
zbMath0644.18003MaRDI QIDQ3786612
Publication date: 1987
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
completenesspolymorphismfull embeddingtopos modelhyperdoctrine modelsecond-order typed \(\lambda \)-calculus
Specification and verification (program logics, model checking, etc.) (68Q60) Categorical logic, topoi (03G30) Topoi (18B25) Combinatory logic and lambda calculus (03B40) Theory of computing (68Q99)
Related Items
The Girard-Reynolds isomorphism, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, Parametricity as isomorphism, On completeness and cocompleteness in and around small categories, Logical systems. I: Internal calculi., A higher-order calculus and theory abstraction, Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus, On the semantics of the universal quantifier, The Girard-Reynolds isomorphism (second edition), Singleton, union and intersection types for program extraction, An extension of system F with subtyping, Independence results for calculi of dependent types, Dictoses, Parametric Polymorphism — Universally, Intuitive counterexamples for constructive fallacies, Covariant types, Internal enriched categories, Types, abstraction, and parametric polymorphism, part 2, What should a generic object be?, Alpha conversion, conditions on variables and categorical logic, Universal properties for universal types in bifibrational parametricity, Bifibrational functorial semantics of parametric polymorphism, A modest model of records, inheritance, and bounded quantification, A characterization of lambda definability in categorical models of implicit polymorphism, Equational theories for inductive types, Categorical models of polymorphism, Second-order type isomorphisms through game semantics, Realizability models and implicit complexity, Comprehension categories and the semantics of type dependency, Linear realizability and full completeness for typed lambda-calculi, A game semantics for generic polymorphism, Unnamed Item, HasCasl: integrated higher-order specification and program development, Extensional models for polymorphism, The semantics of second-order lambda calculus, Functorial polymorphism, From constructivism to computer science, Domain theoretic models of polymorphism, Realizability models for BLL-like languages, Some properties of Fib as a fibred \(2\)-category
