- 10:30 Coffee
- 11:00 Jens Palsberg (UCLA): Typed Self-Interpretation by Pattern Matching
- 12.00 Gilad Bracha (Google): Dart: An Optionally-typed Language for the Web
- Break
- 14:00 Coffee
- 14:30 Rustan Leino (Microsoft Research): Induction in the program verifier Dafny
- 15:30 James Noble (Victoria University of Wellington) Grace: a new object-oriented educational programming language
Abstracts:
Title: Typed Self-Interpretation by Pattern Matching
Speaker: Jens Palsberg (UCLA, University of California, Los Angeles)
Self-interpreters can be roughly divided into two sorts: self-recognisers that recover the input program from a canonical representation, and self-enactors that execute the input program. Major progress for statically-typed languages was achieved in 2009 by Rendel, Ostermann, and Hofer who presented the first typed self-recogniser that allows representations of different terms to have different types. A key feature of their type system is a type:type rule that renders the kind system of their language inconsistent.
I will present the first statically-typed language that not only allows representations of different terms to have different types, and supports a self-recogniser, but also supports a self-enactor. Our language is a factorisation calculus in the style of Jay and Given-Wilson, a combinatory calculus with a factorisation operator that is powerful enough to support the pattern-matching functions necessary for a self-interpreter. This allows us to avoid a type:type rule. Indeed, the types of System F are sufficient. We have implemented our approach and our experiments support the theory.
Title: Induction in the program verifier Dafny
Speaker: K. Rustan M. Leino (Microsoft Research Redmond)
Mechanical proof assistants have always had support for inductive proofs and can be used to verify programs. For many applications, program verifiers that are instead based on satisfiability modulo theories (SMT) solvers can offer a higher degree of automation. However, SMT solvers do not natively support induction, so inductive proofs require some encoding into the SMT solver’s input.
In this talk, I show how the programming language and verifier Dafny incorporates support for automatic induction via an SMT solver. The simple induction tactic decides when and how to apply induction, but does not attempt more difficult tasks like lemma discovery. Still, the tactic has shown to be useful in verifying simple inductive theorems, like those that can occur during program verification.
Title Dart, An Optionally-typed Language for the Web
Speaker: Gilad Bracha (Google)
Dart is a new programming language being developed at Google, focused on web programming. Concurrency and security in Dart are based on an actor-like concept of isolates. Dart supports optional types, and we are considering pluggable types as well. We are also developing a mirror based reflective API for Dart. The talk will provide an overview of Dart, and expand on its more interesting features as time permits.
Title: Grace: a new object-oriented educational programming language
Speaker: James Noble (Victoria University of Wellington)
We are engaged in the design of a new object-oriented educational programming language called Grace. Our motivation is frustration with available languages, most of which are approaching 20 years old. In this talk, I’ll outline the principal features of Grace, discuss open issues, and listen to your reactions while all the choices are still on the table. In particular, I’ll give some examples from the design process so far, showing how conceptually orthogonal design decisions all too easily end up as tightly coupled gordian knots.