PLDI
2011
ACM
13 years 3 months ago
2011
ACM
Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the...
LICS
2010
IEEE
13 years 10 months ago
2010
IEEE
Let R be a class of generators of node-labelled infinite trees, and L be a logical language for describing correctness properties of these trees. Given R R and L, we say that R ...
ESOP
2008
Springer
14 years 2 months ago
2008
Springer
Abstract. We survey recent developments in an approach to the verification of higher-order computation based on game semantics. Higherorder recursion schemes are in essence (progra...
FOSSACS
2010
Springer
14 years 4 months ago
2010
Springer
A new framework for higher-order program verification has been recently proposed, in which higher-order functional programs are modelled as higher-order recursion schemes and then ...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addi...
PPDP
2009
Springer
14 years 7 months ago
2009
Springer
We propose a novel type-based model checking algorithm for higher-order recursion schemes. As shown by Kobayashi, verification problems of higher-order functional programs can ea...
CALCO
2009
Springer
14 years 7 months ago
2009
Springer
Higher-order recursion schemes are equations defining recursively new operations from given ones called “terminals”. Every such recursion scheme is proved to have a least inte...