Type systems for dummies
Abstract
References
Index Terms
- Type systems for dummies
Recommendations
Setoid Type Theory—A Syntactic Translation
Mathematics of Program ConstructionAbstractWe introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying function extensionality, propositional extensionality and a definitional computation rule for transport. ...
Normalization by evaluation for sized dependent types
Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional ...
Irrelevance in type theory with a heterogeneous equality judgement
FOSSACS'11/ETAPS'11: Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of softwareDependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To obtain reasonable performance of not only the compiled program but also the type checker such static ...
Comments
Information & Contributors
Information
Published In

Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
Acceptance Rates
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 165Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)0
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in