Quotient types: A modular approach

DOI10.1007/3-540-45685-6_18MaRDI QIDQ4484345zbMATH OpenFDO

Authors Aleksey Nogin

Publication date 12 June 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm, https://hdl.handle.net/1813/5849

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Quotients, inductive types, and quotient inductive types
• Type theory in type theory using quotient inductive types
• Normalized types
• Pragmatic quotient types in Coq
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

Cited in

(11)

• A language with type-dependent equality
• Invariants for the FoCaL language
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Modular types in some supersimple theories
• Formalizing type operations using the ``image type constructor
• About effective quotients in constructive type theory
• Quotients of bounded natural functors
• Quotients of Bounded Natural Functors
• Quotients by idempotent functions in Cedille
• Pragmatic quotient types in Coq
• Quotients over Minimal Type Theory

This page was built for publication: Quotient types: A modular approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484345)