Published: 14th February 2012 DOI: 10.4204/EPTCS.77 ISSN: 2075-2180 |
Preface | |
Invited Presentation: Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types Andreas Abel | 1 |
Invited Presentation: Higher-Order Model Checking C.-H. Luke Ong | 13 |
Characteristic Formulae for Relations with Nested Fixed Points Luca Aceto and Anna Ingólfsdóttir | 15 |
IO vs OI in Higher-Order Recursion Schemes Axel Haddad | 23 |
Initial Semantics for Strengthened Signatures André Hirschowitz and Marco Maggesi | 31 |
Model-Checking the Higher-Dimensional Modal mu-Calculus Martin Lange and Etienne Lozes | 39 |
Cut-elimination for the mu-calculus with one variable Grigori Mints and Thomas Studer | 47 |
Structured general corecursion and coinductive graphs [extended abstract] Tarmo Uustalu | 55 |
This volume contains the proceedings of the Eighth Workshop on Fixed Points in Computer Science which took place on 24 March 2012 in Tallinn, Estonia as an ETAPS-affiliated workshop. Past workshops have been held in Brno (1998, MFCS/CSL workshop), Paris (2000, LC workshop), Florence (2001, PLI workshop), Copenhagen (2002, LICS (FLoC) workshop), Warsaw (2003, ETAPS workshop), Coimbra (2009, CSL workshop), and Brno (2010, MFCS-CSL workshop).
Fixed points play a fundamental role in several areas of computer science and logic by justifying induction and recursive definitions. The construction and properties of fixed points have been investigated in many different frameworks such as: design and implementation of programming languages, program logics, and databases. The aim of this workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points.
We wish to thank Andreas Abel (Ludwig-Maximilians-Universität) and Luke Ong (University of Oxford) for accepting our invitation to speak at this workshop and for their contributions to these proceedings. We also thank all those authors who have submitted extended abstracts for evaluation to the program committee. Thanks are also due to Keiko Nakata and Tarmo Uustalu for their support of this workshop, both organizational and financial, and to Zoltán L. Németh for his help with the workshop's web pages and with assembling these proceedings.
This workshop received support from the Estonian Centre of Excellence in Computer Science (EXCS), a project financed by the European Regional Development Fund (ERDF). We thank them for their support.
Zoltán Ésik and Dale Miller
Recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. An old model of computation much studied in the Seventies, there has been a revival of interest in recursion schemes as generators of infinite structures (such as infinite trees) with rich algorithmic properties. Higher-order model checking - the model checking of trees generated by higher-order recursion schemes - is a natural generalisation of finite-state and pushdown model checking; it can serve as a basis for software model checkers for functional languages such as ML and Haskell.
After a quick survey of expressivity and decidability results in higher-order model checking, we present our recent application to the model checking of higher-order functional programs with pattern-matching algebraic data types. We are concerned with the (undecidable) verification problem: given a correctness property φ, a functional program P and a regular input set I, does every term that is reachable from I under rewriting by P satisfy φ? Our solution is a sound semi-algorithm (i.e. given a no-instance of the verification problem, the method is guaranteed to terminate) which uses counterexample-guided abstraction refinement, and is based on a backend model checker.
Given a trivial automaton (i.e. Buechi tree automaton with a trivial acceptance condition) and a non-deterministic higher-order recursion scheme with case construct over finite date-types, the model checker decides if the language of trees generated by the scheme is accepted by the automaton. The model checking problem is characterised by an intersection type system extended with a carefully restricted form of union types; the decision procedure is based on the notion of traversal from game semantics. We demonstrate the effectiveness of an implementation of the algorithm on abstract models of functional programs obtained from an abstraction-refinement procedure.
This talk is based on joint work with Steven Ramsay and Robin Neatherway.