Invited Talks

• Ranjit Jhala (Department of Computer Science and Engineering, University of California, San Diego)
  • Title: Liquid Types For Haskell
  • Abstract: We present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses “refinement types”, a restricted form of dependent types where relationships between values are encoded by decorating types with logical predicates drawn from an efficiently SMT decidable theory (of arithmetic and uninterpreted functions). In this talk, we will describe the key ingredients of LiquidHaskell. First, we will present a rapid overview of liquid refinement types, including SMT solver based (decidable) subtyping, and inference. Decidability is achieved by eschewing the use of arbitrary terms inside types, and the use of indices to encode rich properties of data.
    Second, we will show how to recover some of the expressiveness lost by restricting the logic, with two new techniques: measures which encode structural properties of values and abstract refinements which enable generalization (i.e. quantification) over refinements.
    Third, we will discuss the curious interaction of laziness and refinement typing. In a nutshell, the technique of refinement typing can be viewed as a type-based generalization of Floyd-Hoare logics. Surprisingly, we demonstrate that under non-strict evaluation, these logics (and hence, classical refinement typing) is unsound, due to the presence of potentially divergent sub-computations. Fortunately, we show how soundness can be recovered with a termination analysis, itself, circularly bootstrapped off refinement typing.
    We have used LiquidHaskell to verify safety, functional correctness and termination properties of real-world Haskell libraries totalling more than 10,000 lines of code. Time permitting, we will present a demonstration of the tool and a few short case studies illustrating its use.
    (Joint work with Niki Vazou and Eric Seidel and Patrick Rondon)
• Gabriele Keller (School of Computer Science and Engineering, The University of New South Wales)
  • Title: Programming Language Methodologies for Systems Verification
  • Abstract: The need for correct and secure systems is becoming more acute as software is impacting a greater part of our daily life. Formal verification is one method to improve on the status quo. In many cases, however, the costs are still simply too high.
    In this talk, I will present an outline of our approach to achieving a fully verified operating system at acceptable costs. It is based on combining insights from systems, formal methods and programming language research. I will give a brief overview of the history of the project and the goals already achieved, followed by a more detailed look at a specific subproject, namely file system verification. In particular, I will describe the role of two distinct domain-specific programming languages in this framework.
• Shin-ya Katsumata (Research Institute for Mathematical Sciences, Kyoto University)
  • Title: Relating Computational Effects by TT-Lifting
  • Abstract: When two interpretations of a programming language are given, we are naturally interested in the problem of establishing a relationship between these interpretations. A representative case is the computational adequacy of PCF, which compares the denotational semantics and the operational semantics of PCF.
    Problems of this sort are also seen in monadic representations of computational effects. They vary a lot depending on the combination of a computational effect, two monadic representations of it and a relationship between these monadic representations. For instance,
    1. A simple problem is to compare two monadic representations of nondeterministic computations using the powerset monad and the list monad.
    2. Filinski gave a formal relationship between the monadic representation and the CPS representation of call-by-value programs [1]. This is to compare representations of computational effects by a monad T and the continuation monad (- ⇒ TR) ⇒ TR.
    3. Wand and Vaillancourt compared two monadic representations of backtracking computations using the stream monad and the 2-CPS monad [6].
    We aim to solve these problems in a uniform manner. We give a set of conditions to show that a given relationship holds between two monadic interpretations of a call-by-value functional language. These conditions are applicable to a wide range of problems relating computational effects. The proof of this result employs the categorical TT-lifting [2], which is a semantic analogue of Lindley and Stark's leapfrog method [4, 5], and offers a flexible method to construct logical relations for monads. This talk is based on the paper [3].
    1. Andrzej Filinski. Representing monads. In Proc. POPL 1994, pages 446-457, 1994.
    2. Shin-ya Katsumata. A semantic formulation of TT-lifting and logical predicates for computational metalanguage. In Proc. CSL 2005, volume 3634 of LNCS, pages 87-102. Springer, 2005.
    3. Shin-ya Katsumata. Relating computational effects by TT-lifting. Inform. and Comput. (Special issue on ICALP 2011), 222:228-246, 2013.
    4. Samuel Lindley. Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh, 2004.
    5. Samuel Lindley and Ian Stark. Reducibility and TT-lifting for computation types. In Proc. TLCA, pages 262-277, 2005.
    6. Mitchell Wand and Dale Vaillancourt. Relating models of backtracking. In Proc. ICFP 2004, pages 54-65, 2004.

---

flops2014