A Bidirectional Refinement Type System for LF

William Lovas, Frank Pfenning. A Bidirectional Refinement Type System for LF. Electronic Notes in Theoretical Computer Science, 196:113-128, 2008. [doi]

Abstract

Abstract is missing.