Wed 10 Jan 2018 15:50 - 16:15 at Watercourt - Types Chair(s): Thorsten Altenkirch

Ornaments are a way to describe changes in datatype definitions reorganizing, adding, or dropping some pieces of data so that functions operating on the bare definition can be partially and sometimes totally lifted into functions operating on the ornamented structure. We propose an extension of ML with higher-order ornaments, demonstrate its expressiveness with a few typical examples, study the metatheoretical properties of ornaments, and describe their elaboration process. We formalize ornamentation via an a posteriori abstraction of the bare code, called a generic lifting, which lives a meta-language above ML. The lifted code is obtained by application of the generic lifting to well-chosen arguments, followed by staged reduction, and some remaining simplifications. We use logical relations to closely relate the ornamented code to the bare code.

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

15:50 - 17:30
TypesResearch Papers at Watercourt
Chair(s): Thorsten Altenkirch University of Nottingham
15:50
25m
Talk
A Principled approach to Ornamentation in ML
Research Papers
16:15
25m
Talk
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
Research Papers
William J. Bowman Northeastern University, USA, Youyou Cong Ochanomizu University, Japan, Nick Rioux Northeastern University, USA, Amal Ahmed Northeastern University, USA
Link to publication DOI Pre-print
16:40
25m
Talk
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Research Papers
Ondřej Kunčar Technische Universität München, Germany, Andrei Popescu Middlesex University, London
17:05
25m
Talk
Univalent Higher Categories via Complete Semi-Segal Types
Research Papers
Paolo Capriotti University of Nottingham, Nicolai Kraus University of Nottingham