2008/01/01 by William Lovas, Frank Pfenning · 14 citations
Computer Science · Mathematics · #Logic, programming, and type systems #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Decidability #Subtyping #Type (biology) #Type theory #Expressive power #Intersection (aeronautics) #Computer science #Dependent type #Programming language #Domain (mathematical analysis) #Theoretical computer science #Mathematics #Algebra over a field #Pure mathematics #Natural deduction
paper · pdf · doi:10.1016/j.entcs.2007.09.021
published in Electronic Notes in Theoretical Computer Science 196, 113-128 (Elsevier BV)
openalex publication_date 2008/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.