Title:         Programming with dependent types using small inversions
Time：     10:00 - 11:30, March 25 Friday ,2016
Location:   Room 201, Math Building
Lecturer： Jean-Francois Monin   University Grenoble Alpes

Biography:

Jean-François Monin is the European Director of Sino-European Lab LIAMA and has been a professor of Computer Science at University Joseph Fourier (now University Grenoble Alpes) since 2003.  From 2009 to 2013 he has been awarded a CNRS research grant in LIAMA and at Tsinghua University.  His main research interests are about formal methods.  He wrote a synthesis book on this topic, after successfully proving the correctness properties of software devices in an industrial framework. He has a long experience with the Coq type-theoretic proof assistant, with applications on distributed algorithms, security issues and embedded software.

Abstract：

Dependent types are a convenient way to describe and program on constrained data-structures. Common examples include lists having a given length, ordered binary trees, typed lambda-terms or expressions, and data packets exchanged in communication protocols.  By inserting assertions in the type itself, the programmer has no way to produce undesired or unsafe values. The main programming languages with this feature are functional languages such as Cayenne, Idris, Epigram, or even Ocaml to a limited extent, and of course the programming language of Coq or of similar type-theoretic proof assistants. Recent research work consider applications for depend types to low-level programming as well.

However, such types are technically more complex to handle and to reason about. In this talk we focus on inductively defined dependent types.

Getting sub-structures of a given data is similar to inverting an inductively defined relation, such as SOS semantics rules.We show that our handcrafted "small inversions" technique naturally generalizes to dependent data-types, providing concise and elegant programming schemes.