Ornaments, which have recently been put in the spotlight [Dagand and McBride, 2014, Ko and Gibbons, 2016], are a way to describe changes in datatype definitions, reorganizing, adding, or dropping some pieces of data. Ornamentation is the process of translating code operating on the original datatype to code operating on the new one. Williams and Rémy have proposed a formalization and an implementation for the ML family of languages. Our work focuses on the opposite transformation, called disornamentation. We generalized the ornamentation framework developed for ML and based on a posteriori abstraction so that both ornamentation and disornamentation become instances of this framework, allowing more expressive relational transformations of datatypes. We have adapted the ornamentation prototype to support such bidirectional transformations and used it to write several typical examples using disornamentation or a combination of ornamentation and disornamentation.
Fri 28 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:30 - 15:10 | |||
13:30 25mTalk | ML as a Tactic Language, Again ML Guido Martínez CIFASIS-CONICET, Argentina, Danel Ahman University of Ljubljana, Victor Dumitrescu , Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Cătălin Hriţcu Inria Paris, Monal Narasimhamurthy , Zoe Paraskevopoulou Princeton University, Clément Pit-Claudel MIT CSAIL, Jonathan Protzenko Microsoft Research, Redmond, Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research File Attached | ||
13:55 25mTalk | Design and verification of functional proof checkers ML Roberto Blanco Inria | ||
14:20 25mTalk | Disornamentation ML | ||
14:45 25mTalk | Generic Programming with Combinators and Objects ML |