Showing cs.LOShow all
3 papers · 1 filter
cs.LO2015
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong +1
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring inform…
cs.LO2011
Refinement Types as Higher Order Dependency Pairs
Cody Roux
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of…
cs.LO2009
On the relation between size-based termination and semantic labelling
Frédéric Blanqui, Cody Roux
We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expr…