View: session overviewtalk overview
13:00 | A Fast Decision Procedure for Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems PRESENTER: Masaomi Yamaguchi ABSTRACT. Uniqueness of normal forms w.r.t. conversion (UNC) of term rewriting systems (TRSs) guarantees that there are no distinct convertible normal forms. It was recently shown that the UNC property of TRSs is decidable for shallow TRSs (Radcliffe et al., 2017). The existing procedure mainly consists of testing whether there exists a counterexample in a finite set of candidates; however, the procedure suffers a bottleneck of having a sheer number of such candidates. In this paper, we propose a new procedure which consists of checking a smaller number of such candidates and enumerating such candidates more efficiently. Correctness of the proposed procedure is proved and its complexity is analyzed. Furthermore, these two procedures have been implemented and it is experimentally confirmed that the proposed procedure runs much faster than the existing procedure. |
13:30 | Strongly Normalizing Higher-Order Relational Queries PRESENTER: Wilmer Ricciotti ABSTRACT. Language-integrated query is a popular and powerful programming construct, which allows database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Moreover, Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and subsequently Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in languages such as Links and F#. However, as we explain, there is no published proof of the central strong normalization property for higher-order nested relational queries: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the TT-lifting approach of Lindley and Stark to accommodate duplicating rewrites. |
14:00 | WANDA - a Higher Order Termination Tool - System description ABSTRACT. Wanda is a fully automatic termination analysis tool for higher-order term rewriting. In this paper, we will discuss the methodology used in Wanda. Most pertinently, this includes a higher-order dependency pair framework and a variation of the higher-order recursive path ordering, as well as some non-termination analysis techniques and delegation to a first-order tool. Additionally, we will discuss how to use Wanda in practice for systems in two different formalisms and present experimental results |
13:00 | Symbolic Execution Game Semantics PRESENTER: Nikos Tzevelekos ABSTRACT. We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the K framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs. |
13:30 | A Probabilistic Higher-order Fixpoint Logic PRESENTER: Yo Mitani ABSTRACT. We introduce PHFL, a probabilistic extension of higher-order fixpoint logic. PHFL may also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and \(\mu^p\)-calculus. We show that PHFL is strictly more expressive than \(\mu^p\)-calculus, and that the PHFL model checking problem for finite Markov chains is undecidable even for the \(\mu\)-only, order-\(1\) fragment of PHFL. Furthermore, we show a translation from Lubarsky's MuArithmetic to PHFL, which implies that PHFL model checking is \(\Pi^1_1\)-hard. As a positive result, we characterize a decidable fragment of the PHFL model checking problems using a novel type system. |
14:00 | Refining Constructive Hybrid Games PRESENTER: Brandon Bohrer ABSTRACT. We extend the constructive differential game logic (\CdGL) of hybrid games with a refinement connective that relates two hybrid games. We use this connective to prove a folk theorem relating hybrid games to hybrid systems. |
14:30 | On Average-Case Hardness of Higher-Order Model Checking PRESENTER: Yoshiki Nakamura ABSTRACT. We study a mixture between the average case and worst case complexities of higher-order model checking, the problem of deciding whether the tree generated by a given λY-term (or equivalently, a higher-order recursion scheme) satisfies the property expressed by a given tree automaton. Higher-order model checking has recently been studied extensively in the context of higher-order program verification. Although the worst-case complexity of the problem is k-EXPTIME complete for order-k terms, various higher-order model checkers have been developed that run efficiently for typical inputs, and program verification tools have been constructed on top of them. One may, therefore, hope that higher-order model checking can be solved efficiently in the average case, despite the worst-case complexity. We provide a negative result, by showing that, under certain assumptions, for almost every term, the higher-order model checking problem specialized for the term is k-EXPTIME hard with respect to the size of automata. The proof is based on a novel intersection type system that characterizes terms that do not contain any useless subterms. |