Categorical logic and type theory

Publication date: 11 February 1999

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

zbMATH Keywords

first-order logic typed lambda-calculus categorical semantics effective topos indexed categories dependent type theory regular categories toposes semantics of programming languages fibred categories coherent categories complete small category of PERs higher-order predicate logic logoses polymorphic type theory

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Topoi (18B25) Fibered categories (18D30)

Related Items

Monoidal Grothendieck construction, Homotopies in Grothendieck fibrations, Coalgebraic Components in a Many-Sorted Microcosm, Type Theoretical Databases, Monoidal reverse differential categories, Linear Dependent Type Theory for Quantum Programming Languages, AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS, Theory Presentation Combinators, Logic in Category Theory, Doctrines, modalities and comonads, Categorifying Computations into Components via Arrows as Profunctors, Six model categories for directed homotopy, Elementary fibrations of enriched groupoids, Latent Fibrations: Fibrations for Categories of Partial Maps, Recognizable languages of arrows and cospans, Parametric Polymorphism — Universally, Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory, Stone Dualities from Opfibrations, Dependently Sorted Logic, Fibered universal algebra for first-order logics, Fundamentals of compositional rewriting theory, The linear-non-linear substitution 2-monad, Compositional Game Theory, Compositionally, A Categorical Aspect of the Analogy Between Quantifiers and Modalities, Elimination of extensionality in Martin-Löf type theory, The monoidal nature of the Feistel-Toffoli construction, The algebra of the Feistel-Toffoli construction, Preservation and reflection of bisimilarity via invertible steps, A UNIVERSAL CHARACTERIZATION OF STANDARD BOREL SPACES, Martin-Löf identity types in C-systems, Unnamed Item, On effective descent $\mathcal{V}$-functors and familial descent morphisms, A general framework for the semantics of type theory, CHAD for expressive total languages, Unnamed Item, Unnamed Item, Linearizing Combinators, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Universal properties for universal types in bifibrational parametricity, A model of guarded recursion with clock synchronisation, Bifibrational functorial semantics of parametric polymorphism, Coherence Spaces and Uniform Continuity, Unnamed Item, Unnamed Item, A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators, A type theory for synthetic $\infty$-categories, Sets and Descent, Displayed Categories, Coinduction in Flow: The Later Modality in Fibrations, LOGICAL CONTEXTUALITY IN FREGE, Distributed Modal Logic, Traces for coalgebraic components, Up-To Techniques for Behavioural Metrics via Fibrations, An Isbell duality theorem for type refinement systems, Partiality, State and Dependent Types, Unnamed Item, Relating Computational Effects by ⊤ ⊤-Lifting, Codensity Lifting of Monads and its Dual, Initial Algebras of Terms with Binding and Algebraic Structure, Deforestation, program transformation, and cut-elimination, A Calculus of Terms for Coalgebras of Polynomial Functors, Modal Languages for Coalgebras in a Topological Setting, Sets in homotopy type theory, Univalence for inverse diagrams and homotopy canonicity, Unnamed Item, Displayed Categories, Unnamed Item, A metalanguage for guarded iteration, Proof theory in the abstract, Weakest preconditions in fibrations, Monoidal-closed categories of tree automata, Pointers in Recursion: Exploring the Tropics, Weak ω-Categories from Intensional Type Theory, Kripke Semantics for Martin-Löf’s Extensional Type Theory, The generalised type-theoretic interpretation of constructive set theory, Categorical semantics for arrows, Two-dimensional models of type theory, Dynamic game semantics, Unnamed Item, Coinductive predicates and final sequences in a fibration, Dwyer–Kan homotopy theory for cyclic operads, Greatest Bisimulations for Binary Methods, Factorization systems and fibrations, Multiplicative Linear Logics and Fibrations, Joyal's arithmetic universes via type theory, Unnamed Item, Type Theory and Homotopy, Coalgebras as Types Determined by Their Elimination Rules, Homotopical Categories of Logics, Categories with Families: Unityped, Simply Typed, and Dependently Typed, A Diagrammatic Logic for Object-Oriented Visual Modeling, FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION, Algebraic Databases, Network Models, CATEGORICAL HARMONY AND PATH INDUCTION, MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS, Divergences on monads for relational program logics, An intuitionistic set-theoretical model of fully dependent CC, What should a generic object be?, Towards a constructive simplicial model of Univalent Foundations, Up-to techniques for behavioural metrics via fibrations, Coinductive predicates and final sequences in a fibration, Automata-theoretic semantics of idealized Algol with passive expressions, Logical relations and parametricity -- a Reynolds programme for category theory and programming languages, Modeling Martin-Löf type theory in categories, Coalgebraic update lenses, A characterisation of elementary fibrations, Paracategories. I: Internal paracategories and saturated partial algebras, Paracategories. II: Adjunctions, fibrations and examples from probabilistic automata theory, The effects of effects on constructivism, Condition/decision duality and the internal logic of extensive restriction categories, Deriving logical relations from interpretations of predicate logic, Weakest preconditions in fibrations, Computational adequacy for recursive types in models of intuitionistic set theory, Morphisms of open games, Cartesian integral categories and contextual integral categories, Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics, A simplicial foundation for differential and sector forms in tangent categories, Relational lattices: from databases to universal algebra, Stone dualities from opfibrations, Modules over quantaloids: applications to the isomorphism problem in algebraic logic and $\pi$-institutions, Logical systems. I: Internal calculi., On inverse operators in dynamic epistemic logic, Dialectica logical principles, A fibrational framework for possible-world semantics of \textsc{Algol}-like languages, Internal diagrams and archetypal reasoning in category theory, Quotient completion for the foundation of constructive mathematics, Martin-Löf complexes, Internal languages of finitely complete $(\infty , 1)$-categories, Involutive categories and monoids, with a GNS-correspondence, Coreflections in algebraic quantum logic, Fibred 2-categories and bicategories, Toward weakly enriched categories: co-Segal categories, An algebraic theory for data linkage, Generic weakest precondition semantics from monads enriched with order, Dijkstra and Hoare monads in monadic computation, Modular operads and the nerve theorem, A domain-theoretic semantics of lax generic functions., Presheaf models for CCS-like languages, A characterization of generalized existential completions, Bifibrations and weak factorisation systems, A model of guarded recursion via generalised equilogical spaces, Voltage lifts of graphs from a category theory viewpoint, Probabilistic systems coalgebraically: a survey, System theory for system identification., A characterization of those categories whose internal logic is Hilbert's $\varepsilon$-calculus, Elementary doctrines as coalgebras, The categorical imperative: category theory as a foundation for deontic logic, Enriched duality in double categories: $\mathcal{V}$-categories and $\mathcal{V}$-cocategories, Differential equations in a tangent category. I: Complete vector fields, flows, and exponentials, Parametricity for primitive nested types, A general semantic construction of dependent refinement type systems, categorically, Graded Hoare logic and its categorical semantics, Equality of proofs for linear equality, Modular construction of complete coalgebraic logics, Domain-theoretical models of parametric polymorphism, Factorizing the $\mathbf{Top}$-$\mathbf{Loc}$ adjunction through positive topologies, The algebra of partial equivalence relations, Fibrational modal type theory, Duality in non-abelian algebra. III. Normal categories and 0-regular varieties, Comprehensive factorisation systems, Synthetic domain theory and models of linear Abadi {\&} Plotkin logic, Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study, Coalgebras for Binary Methods: Properties of Bisimulations and Invariants, A general account of coinduction up-to, The identity type weak factorisation system, Splitting idempotents in a fibered setting, Revisiting the categorical interpretation of dependent type theory, The rôle of categorical structures in infinitesimal calculus, Monads in double categories, A co-free construction for elementary doctrines, Unifying exact completions, Probabilities, distribution monads, and convex categories, The proof monad, Quantum logic in dagger kernel categories, Realizability models refuting Ishihara's boundedness principle, Generalising canonical extension to the categorical setting, Cartesian closed Dialectica categories, Fibrational bisimulations and quantitative reasoning, Comprehensive Parametric Polymorphism: Categorical Models and Type Theory, Guarded Dependent Type Theory with Coinductive Types, Dependent Types and Fibred Computational Effects, Coherence in linear predicate logic, Dynamical systems and sheaves, A Classical Propositional Logic for Reasoning About Reversible Logic Circuits, Quantum Logic in Dagger Kernel Categories, Relating Toy Models of Quantum Computation: Comprehension, Complementarity and Dagger Mix Autonomous Categories, A categorical outlook on relational modalities and simulations, A minimalist two-level foundation for constructive mathematics, Equilogical spaces, On the algebraic structure of declarative programming languages, A categorical framework for typing CCS-style process communication, Comprehension for Coalgebras, Categories with families and first-order logic with dependent sorts, Containers: Constructing strictly positive types, Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic, Corecursion up-to via causal transformations, Univalence and completeness of Segal objects, A natural semantics of first-order type dependency, Elementary axioms for local maps of toposes, The Grothendieck construction for model categories