×

A bidirectional refinement type system for LF. (English) Zbl 1278.03060

Pientka, B. (ed.) et al., Proceedings of the second international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2007), Bremen, Germany, July 15, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 196, 113-128 (2008).
Summary: We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are bidirectional, leading to a straightforward proof of decidability of type-checking even in the presence of intersection types. Because we insist on canonical forms, structural rules for subtyping can now be derived rather than being assumed as primitive. We illustrate the expressive power of our system with several examples in the domain of logics and programming languages.
For the entire collection see [Zbl 1276.68025].

MSC:

03B70 Logic in computer science
68N15 Theory of programming languages

Software:

Forsythe; Twelf
PDFBibTeX XMLCite
Full Text: Link