Step-Indexed Normalization for a Language with General Recursion
The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments—a _logical_ fragment where every term normalizes and which is consistent when interpreted as a logic, and a _programmatic_ fragment with general recursion and oth...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1202.2918v1 |