Setoids in type theory

DOI10.1017/S0956796802004501zbMath1060.03030OpenAlexW1988136938WikidataQ56430943 ScholiaQ56430943MaRDI QIDQ4457833

Gilles Barthe, Olivier Pons, Venanzio Capretta

Publication date: 17 March 2004

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796802004501

zbMATH Keywords

dependent type theorypartial setoidrepresentation of sets as setoidstotal setoid

Mathematics Subject Classification ID

Related Items (26)

Normalization by evaluation and algebraic effects ⋮ Towards Measurable Types for Dynamical Process Modeling Languages ⋮ Invariants for the FoCaL language ⋮ Packaging Mathematical Structures ⋮ Quotient completion for the foundation of constructive mathematics ⋮ Unnamed Item ⋮ Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator ⋮ Meaning explanations at higher dimension ⋮ Coalgebras in functional programming and type theory ⋮ Unnamed Item ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ Proof-Relevant Logical Relations for Name Generation ⋮ Unifying exact completions ⋮ A computer-verified monadic functional implementation of the integral ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Unnamed Item ⋮ Point-Free, Set-Free Concrete Linear Algebra ⋮ Finite Groups Representation Theory with Coq ⋮ Type classes for mathematics in type theory ⋮ W-types in setoids ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Formalization of universal algebra in Agda ⋮ Extending Sledgehammer with SMT solvers ⋮ Formalizing complex plane geometry

This page was built for publication: Setoids in type theory