scientific article; zbMATH DE number 1927427

zbMATH Open1013.68198MaRDI QIDQ4484345FDOQ4484345

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

Title of this publication is not available (Why is that?)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (11)

• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Pragmatic quotient types in Coq
• A language with type-dependent equality
• Formalizing type operations using the ``image type constructor
• Quotients over Minimal Type Theory
• Quotients of Bounded Natural Functors
• Invariants for the FoCaL language
• Title not available (Why is that?)
• Quotients by idempotent functions in Cedille
• Title not available (Why is that?)
• Modular types in some supersimple theories

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)