Vous êtes ici

Refinement types for stream processing languages

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
https://www.inria.fr/equipes/tea
Directeur de thèse
Jean-Pierre Talpin
Co-directeur(s), co-encadrant(s)
Contact(s)
Sujet de thèse
Descriptif


Context

Advances in both type theory and SAT-based formal verification have led to implementation of the program as proof paradigm using the notion of refinement type.  A refinement type x:t|p  defines the data type t of values named x together with a property p that specifies properties of x within the domain of t and/or the context in which that value is defined.  “clean slate” programming languages such as Liquid Haskell, F*, and many more, implement specification, inference and/or proof of refinement types using SAT-SMT verification (Z3) and proof engines (Coq).

Objective

The aim of the Thesis is to design and implement a domain-specific language for stream processing using refinement types to infer and verify symbolic and quantitative properties (determinism, schedulability, memory usage).  A stream processing language usually comes in the form of simple block-diagrams that define computation and flow of data within a system. Here, just as the many extensions of Haskell with streams, we wish to take advantage of the more natural algorithmic style of functional languages. Ideally, we will base our development on an intermediate representation with no or stack-based memory management and first-order functions, in order to guarantee efficient code or hardware generation.

Profil


We are looking for a talented PhD with demonstrated impact to both theory and implementation of type theory, programming language design, concurrency theory. This PhD proposal is in the frame of Inria's associate team Composite with UC San Diego MESL and project-team TEA.

Bibliographie

•    “Liquid Types” P. Rondon, M. Kawaguci, R. Jahla. the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2008.
•    “Refinement Types for Haskell”. Niki Vazou, Eric Seidel, Ranjit Jhala, Dimitris Vytiniotis, Simon Peyton-Jones. 19th ACM International Conference on Functional Programming, 2014.
•    “Asynchronous liquid separation types”. J. Kloos, R. Majumdar, and V. Vafeiadis. 29th European Conference on Object-Oriented Programming, 2015.
•    “Verified Low-Level Programming Embedded in F∗”. Karthikeyan Bhargavan et al. Certified programs and proofs. ACM, 2017.
•    “Dependent Types and Multi-Monadic Effects in F*”. N; Swamy et al. Symposium on Principles of Programming Languages. ACM, 2016.
•    “Stream fusion, to completeness”.  O.  Kiselyov, A. Biboudis, N. Palladinos, and YaY.nnis Smaragdakis. 44th ACM SIGPLAN Symposium on Principles of Programming Languages. ACM, 2017
•    "Towards refinement types for time-dependent data-flow networks". J.-P. Talpin, P. Jouvelot, S. Shukla. 13th ACM-IEEE Conference on Methods and Models for System Design (MEMOCODE'15). IEEE, 2015.
•    "Region-based memory management". Tofte, M., Talpin, J.-P. Information and Computation, Vol. 132, pages 109-176. Academic Press, 1997.

 

Début des travaux: 
09/2017
Mots clés: 
type theory, programming languages, stream processing, code generation
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes