This talk gives an overview of our recent project to construct a software model checker for ML based on higher-order model checking. Using higher-order model checking, one can decide various properties of simply-typed, higher-order, boolean functionals programs with recursion. After a brief introduction to higher-order model checking, we show how to combine it with predicate abstraction and CEGAR to construct a software model checker, and discuss ongoing and future work.
This is a joint work with Ryosuke Sato and Hiroshi Unno.
SML# is a new generation of Standard ML being developed at RIEC, Tohoku University. Its goal is to provide moderate but practically important features including:
SML# has been developed jointly with several people including Katsuhiro Ueno, Huu-Duc Nguyen, Liu Bochao, Kiyoshi Yamatodani, and Satoshi Osaka.
We present an adaptation of a well-known generic programming technique, often referred to as “Scrap Your Boilerplate”, or SYB, to Objective Caml language. Since the original implementation for Haskell essentially relies on the presence of type classes, the first task in the course of adaptation is to express the main primitives of this approach in a way natural for Objective Caml. Besides that we make use of specialization and continuation-passing style (CPS) to improve the performance of our implementation. CPS is used as a common way to provide a tail-recursive implementation while specialization allows us to lift type-discriminated computations (natural to SYB) from the data level to the type level. As a result the presented version of SYB demonstrates good performance in comparison with non-generic hand-written code.
Computational problems that involve dynamic data have been an important subject of study in programming languages. Recent advances in self-adjusting computation have developed techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. But these techniques have required an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create and operate on data that can change over time. Our paper, “Implicit Self-Adjusting Computation for Purely Functional Programs” (ICFP '11), describes the theory underlying implicit self-adjusting computation, where the programmer need only annotate the (top-level) input types of the programs to be translated. A type-directed translation rewrites the (purely functional) source program into an explicitly self-adjusting target program. The subject of this talk is a prototype implementation (an extension of MLton) and experimental results that are competitive with explicitly self-adjusting handwritten code.
The contribution of this work is threefold. First, we offer an OCaml unmarshaling algorithm that uses a lightweight type-directed description of the expected structure of data to make consistency checks. The second contribution is the opportunity to specify functions to be systematically applied on values as they are being unmarshaled. Our third contribution is a type-safe layer for these functions and for the unmarshaling algorithm itself.
Generalized Algebraic Datatypes, or GADTs, extend algebraic datatypes by allowing an explicit relation between type parameters and case analysis. They have useful applications, among others for encoding invariants of data structures, or providing tagless data representations.
We have implemented them in OCaml, by directly modifying the type inference engine. We discuss the technical choices involved, and the properties expected to hold. In particular, we have worked on two aspects of inference: principality, which holds only by requiring some derivations to be minimal, and exhaustiveness of pattern-matching, which requires a new notion of incompatibility.
Combining monadic computations may induce a significant syntactic overhead. To allow monadic programming in direct style, we have developed Coco, a type-based tool that automatically rewrites ML code inserting necessary binds, unit, and morphisms between monads. This tool demonstration will show how to take advantage of Coco to facilitate using monadic libraries in practice, and will discuss possible future development of Coco to fit the actual needs of programmers.
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi's intersection type-based model checking technique. We show that an implementation of this algorithm, THORS, performs well on a number of small examples and we demonstrate how it can be used to verify liveness properties of OCaml programs. Example properties include statements such as “all opened sockets are eventually closed” and “the lock is held until the file is closed”.
In a paper at ICFP 2008, we proposed a novel module system design called MixML. MixML synthesizes ML modules and Bracha-style “mixin” modules in order to provide a seamless integration of hierarchical module composition, translucent ML-style data abstraction, and mixin-style recursive linking of separately compilable modules. However, the original paper (and conference talk) focused primarily on the design and static semantics of MixML. Little attention was paid to its operational semantics, which was defined (in the appendix) via a rather involved destination-passing-style elaboration translation into RTG, a type system for recursively-defined ADTs that was developed previously by Dreyer (JFP 2007).
In the last few years, we have made a variety of improvements to the semantics of MixML and RTG, which will be described in an extended journal article that we are submitting for publication. These improvements include the following:
There have been many researches on helping programmers to locate and fix type errors. Among them, Chitil proposed an interactive type debugger. The main idea of his system is to make a type inference tree compositional and move through the tree using programmer's answers to locate type errors. Chitil's system is attractive because we are navigated to the source of an error simply by answering questions. However, it has not been used in practise so far. In this paper, we show extension of the type debugger needed to use it for beginners and report on our initial experience of using it in the introductory OCaml course in Ochanomizu University.
Camomile is a Unicode library that has been actively developed for OCaml since 2001. In this presentation, we give a bird's-eye view of interface and implementation of Camomile, and report on the lesson learned from the project continuing for nearly 10 years. This presentation should provide the basic idea behind Camomile, thus complement the detailed API documentation given by ocamldoc.http://conway.rutgers.edu/ml2011/abstracts.html