scientific article; zbMATH DE number 1927427

MaRDI QIDQ4484345zbMATH OpenFDO

Authors Aleksey Nogin

Publication date 12 June 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm

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
• scientific article; zbMATH DE number 1841843
• 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
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• 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:

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