This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the...
Jean-Baptiste Tristan, Paul Govereau, Greg Morrise...
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 ...
Christopher H. Broadbent, Arnaud Carayol, C.-H. Lu...
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...
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 ...
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...
Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong...
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...
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...