Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 15:43 - 16:06 at Aurora Borealis - Types Chair(s): Zoe Paraskevopoulou

Modern functional programming languages, such as Haskell or OCaml, use sophisticated forms of type inference. While an important topic in the Programming Languages research, there is little work on the mechanization of the metatheory of type inference in theorem provers. In particular we are unaware of any complete formalization of the type inference algorithms that are the backbone of modern functional languages.

This paper presents the first full mechanical formalization of the metatheory for higher-ranked polymorphic type inference. The system that we formalize is the bidirectional type system by Dunfield and Krishnaswami (DK). The DK type system has two variants (a declarative and an algorithmic one) that have been manually proven sound, complete and decidable. We present a mechanical formalization in the Abella theorem prover of DK’s declarative type system with a novel algorithmic system. We have a few reasons to use a new algorithm. Firstly, our new algorithm employs worklist judgments, which allow precise capture of the scope of variables and simplify the formalization of scoping in a theorem prover. Secondly, while DK’s original formalization comes with very well-written manual proofs, there are several details missing and some incorrect proofs, which complicate the task of writing a formal proof. Despite the use of a different algorithm we prove the same results as DK, although with significantly different proofs and proof techniques. Since such type inference algorithms are quite subtle and have a complex metatheory, mechanical formalizations are an important advance in type-inference research.

Wed 21 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:20 - 16:30
TypesResearch Papers at Aurora Borealis
Chair(s): Zoe Paraskevopoulou Princeton University
15:20
23m
Talk
Mixed Linear and Non-linear Recursive Types
Research Papers
Bert Lindenhovius Tulane University, Michael Mislove Tulane, Vladimir Zamdzhiev Inria Nancy
15:43
23m
Talk
A Mechanical Formalization of Higher-Ranked Polymorphic Type InferenceDistinguished Paper
Research Papers
Zhao Jinxu , Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
16:06
23m
Talk
An Efficient Algorithm for Type-Safe Structural Diffing
Research Papers
Victor Cacciari Miraldo Utrecht University, Netherlands, Wouter Swierstra Utrecht University, Netherlands