Sciweavers

ENTCS
2008
116views more  ENTCS 2008»
13 years 12 months ago
A Bidirectional Refinement Type System for LF
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 refine...
William Lovas, Frank Pfenning
CORR
2010
Springer
140views Education» more  CORR 2010»
13 years 12 months ago
Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance
Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. We present a system of refinement types for...
William Lovas, Frank Pfenning
POPL
2010
ACM
14 years 9 months ago
Low-Level Liquid Types
We present Low-Level Liquid Types, a refinement type system for C based on Liquid Types. Low-Level Liquid Types combine refinement types with three key elements to automate verifi...
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala