Types for Proofs and Programs

DOI10.1007/b98246zbMath1100.03055OpenAlexW4298423642MaRDI QIDQ5712306

Nicola Gambino, J. M. E. Hyland

Publication date: 23 December 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Related Items (30)

On Church’s thesis in cubical assemblies ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ Actads ⋮ Non-well-founded trees in categories ⋮ Directed Containers as Categories ⋮ Unnamed Item ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ On semiflexible, flexible and pie algebras ⋮ Unnamed Item ⋮ Indexed containers ⋮ The essence of ornaments ⋮ Unnamed Item ⋮ Decomposing Comonad Morphisms. ⋮ Polynomial functors and polynomial monads ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Monads in double categories ⋮ 2-Dimensional Directed Type Theory ⋮ Polynomial functors and opetopes ⋮ Combining effects: sum and tensor ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Unnamed Item ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ A Coalgebraic View of Bar Recursion and Bar Induction ⋮ W-types in setoids ⋮ The universal exponentiable arrow ⋮ Variations on inductive-recursive definitions ⋮ Containers: Constructing strictly positive types ⋮ C-systems defined by universe categories: presheaves ⋮ Unnamed Item ⋮ Constructive Membership Predicates as Index Types

This page was built for publication: Types for Proofs and Programs