Refinement Types for Logical Frameworks
The logical framework LF and its metalogic Twelf can be used to encode and reason about a wide variety of logics, languages, and other deductive systems in a formal, machine-checkable way. Recent studies have shown that ML-like languages can profitably be extended with a notion of subtyping called r...
| Main Author: | |
|---|---|
| Format: | Others |
| Published: |
Research Showcase @ CMU
2010
|
| Subjects: | |
| Online Access: | http://repository.cmu.edu/dissertations/74 http://repository.cmu.edu/cgi/viewcontent.cgi?article=1066&context=dissertations |