Constructing infinitary quotient-inductive types

DOI10.1007/978-3-030-45231-5_14OpenAlexW3021779990MaRDI QIDQ2200826

Andrew M. Pitts, S. C. Steenkamp, Marcelo P. Fiore

Publication date: 23 September 2020

Full work available at URL: https://arxiv.org/abs/1911.06899

zbMATH Keywords

category theorydependent type theoryhigher inductive typesinductive-inductive definitionsquotient typessized types

Mathematics Subject Classification ID

Theory of computing (68Qxx) Theory of software (68Nxx)

Related Items (4)

A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Capturing constrained constructor patterns in matching logic

Uses Software

• Agda

Cites Work

• A feature constraint system for logic programming with entailment
• A formally verified interpreter for a shell-like programming language
• Deciding the first-order theory of an algebra of feature trees with updates
• Feature-constraint logics for unification grammars
• Records for logic programming
• Local Reasoning for the POSIX File System

This page was built for publication: Constructing infinitary quotient-inductive types