Monday
9:30-10:30 Invited talk (chair: Scott Owens)
Conor McBride
Title: Everybody's Got To Be Somewhere
Abstract: Nameless representations of syntax are a staple of programming language implementation. This talk is about a new one. When we represent a syntax as a datatype, we often supply a constructor for variables which allows us to choose one from the variables in scope: that is, we push the information that the other variables are not relevant all the way to the leaves of the syntax tree. I will show a representation where the information about which variables are unused is pulled out towards the root of the syntax tree as far as possible. All the variables in scope for any given subterm are guaranteed to be used somewhere within it. The extra information about what is used where also comes in handy when implementing operations like substitution. This is exactly the sort of invariant that is very easy to get wrong if it has only the force of a moral obligation, but very easy to get right in a modern type system. The approach is not merely useful, but also a fine example of the kind of programming that is no longer too scary to attempt.
10:30-11:00 Break
11:00-12:30 3 papers (chair: Marco Morazan)
Towards Unification for Dependent Types. Ningning Xie and Bruno C. D. S. Oliveira
Combinational and Sequential Circuits in Agda. João Paulo Pizani Flor and Wouter Swierstra
Dynamic Witnesses For Ill-Typed Programs Using Parametric Polymorphism In SML. Thomas Dorrington and Kathryn E Gray
12:30-14:00 Lunch
14:00-15:30 3 papers (chair: Michal Palka)
Towards Multi-tier Time Travel Debugging for the Web. Jeff Horemans, Bob Reynders, Dominique Devriese and Frank Piessens
Discovering the source of Haskell Type Errors using Delta Debugging. Joanna Sharrad and Olaf Chitil
Automatically Introducing Tail Recursion in CakeML. Oskar Abrahamsson
15:30-16:00 Break
16:00-17:00 2 papers (chair: Meng Wang)
Maintaining Separation of Concerns Through Task-Oriented Software Development. Jurriën Stutterheim, Peter Achten and Rinus Plasmeijer
Managing k-ary Trees in Haskell: Towards a Dynamic Data Structure in Functional Programming. Juan Carlos Saenz-Carrasco, Mike Stannett and Paolo Veronelli
Tuesday
10:00-10:30 2 papers (chair: Scott Owens)
Typed Relational Conversion. Petr Lozov, Andrei Vyatkin and Dmitry Boulytchev
10:30-11:00 Break
11:00-12:30 3 papers (chair: Pieter Koopman)
Concurrent System Programming with Effect Handlers. Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhavapeddy, Kc Sivaramakrishnan and Leo White
Cheap Remarks about Concurrent Programs. Michael Walker and Colin Runciman
A Communications Cost Model for a distributed Scheme. John Magnus Morton and Phil Trinder
12:30-14:00 Lunch
14:00-15:30 3 papers (chair: Hans-Wolfgang Loidl)
Memoized Flat Closures for CPS. Marco T. Morazan, Lindsey Reams, Nicholas R. Olson and Shamil Dzhatdoyev
A Task-Based DSL for Microcomputers. Pieter Koopman, Mart Lubbers and Rinus Plasmeijer
Scoping Monadic Relational Database Queries. Anton Ekblad
15:30-16:00 Break
16:00-17:00 2 papers (chair: Meng Wang)
Haskell-tools Refact: a new way to refactor Haskell programs. Boldizsár Németh, Máté Tejfel and Zoltán Kelemen
QuickChecking Patricia Trees. Jan Midtgaard
Wednesday
9:30-10:30 Invited talk (chair: Meng Wang)
Cătălin Hriţcu
Title: Verified Effectful Programming in F*
Abstract: F* is a dialect of ML aimed at program verification that puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification F* programs can be extracted to efficient OCaml, F#, or C code. This enables verifying the functional correctness and security of realistic applications, such as the verified HTTPS stack currently developed in Project Everest.
F*'s extensible effect system allows users to define new monadic effects and monad morphisms for lifting computations from one effect to another. Effectful code is written in direct style and the F* type-checker infers the least effect for each computation and inserts binds and lifts as needed. The effect system also isolates a core dependently-typed language of pure functions that we use to write specifications and proof terms and whose consistency is maintained by a universe hierarchy and a semantic termination check.
Effectful F* code can be verified using two reasoning styles that can also be combined. First, F* code can be verified intrinsically, by decorating ML types with pre- and post-conditions and invariants to specify functional correctness properties. The F* type-checker reduces the correctness of these specifications to SMT queries using a generic weakest-precondition (WP) calculus that combines WPs using effect-specific monads of predicate transformers. F* derives such Dijkstra monads "for free" by applying a
continuation-passing style (CPS) translation to the monadic definitions of the underlying computational effects. Second, terminating F* code can be verified extrinsically, by revealing the underlying monadic representation of its effects and making the most of F*'s support for reasoning about pure programs. This enables the verification of relational properties that describe multiple runs of one or more programs and characterize many useful notions of security, program refinement, and equivalence.
10:30-11:00 Break
11:00-12:30 3 papers (chair: Marco Morazan)
Secure Execution of Financial Contracts on Ethereum. Thorkil Værge, Mads Gram and Omri Ross
On the Implementation of Bignum Multiplication. Shamil Dzhatdoyev and Marco T. Morazan
The CakeML Compiler Explorer: Tracking Intermediate Representations in a Verified Compiler. Rikard Hjort, Jakob Holmgren and Christian Persson
12:30-14:00 Lunch
Outing
Tour of the Cathedral (to be confirmed).
18:00 Dinner
At the Cathedral Lodge.
TPIE Schedule
The TPIE schedule is available here.