- 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
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
- 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.
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 , which is a semantic analogue of Lindley and Stark's leapfrog method
and offers a flexible method to construct logical relations for monads. This talk is based
on the paper .
- A simple problem is to compare two monadic representations of nondeterministic
computations using the powerset monad and the list monad.
- Filinski gave a formal relationship between the monadic representation and the CPS
representation of call-by-value programs . This is to compare representations of
computational effects by a monad T and the continuation monad (- ⇒ TR) ⇒ TR.
- Wand and Vaillancourt compared two monadic representations of backtracking
computations using the stream monad and the 2-CPS monad .
- Andrzej Filinski. Representing monads. In Proc. POPL 1994, pages 446-457, 1994.
- 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.
- Shin-ya Katsumata. Relating computational effects by TT-lifting. Inform. and Comput. (Special issue on ICALP 2011), 222:228-246, 2013.
- Samuel Lindley. Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh, 2004.
- Samuel Lindley and Ian Stark. Reducibility and TT-lifting for computation types. In Proc. TLCA, pages 262-277, 2005.
- Mitchell Wand and Dale Vaillancourt. Relating models of backtracking. In Proc. ICFP 2004, pages 54-65, 2004.