Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

8

CIE
2007
Springer

favoriteEmaildiscussreport

116views Applied Computing» more CIE 2007»

Quotients over Minimal Type Theory

13 years 10 months ago

Quotients over Minimal Type Theory

Download www.math.unipd.it

Abstract. We consider an extensional version, called qmTT, of the intensional Minimal Type Theory mTT, introduced in a previous paper with G. Sambin, enriched with proof-irrelevance of propositions and effective quotient sets. Then, by using the construction of total setoid `a la Bishop we build a model of qmTT over mTT. The design of an extensional type theory with quotients and its interpretation in mTT is a key technical step in order to build a two level system to serve as a minimal foundation for constructive mathematics as advocated in the mentioned paper about mTT.

Maria Emilia Maietti

Real-time Traffic

CIE 2007 | Effective Quotient Sets | Extensional Type Theory | Type Theory MTT |

claim paper

Related Content

» A Design Structure for Higher Order Quotients

» Constructing Polymorphic Programs with Quotient Types

» Structured Formal Development with Quotient Types in IsabelleHOL

» Universal Algebra in Type Theory

» Subtyping in Logical Form

» Pattern minimization problems over recursive data types

» Weighted Bisimulation in Linear Algebraic Form

» Approximations for the Isoperimetric and Spectral Profile of Graphs and Related Parameters

» Markov Random Field Energy Minimization via Iterated Cross Entropy with Partition Strategy

Post Info
More Details (n/a)

Added	07 Jun 2010
Updated	07 Jun 2010
Type	Conference
Year	2007
Where	CIE
Authors	Maria Emilia Maietti

Comments (0)