Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 09:00 - 10:00 at Sala XII - Keynote 1 and Research Paper Chair(s): Magnus O. Myreen

We present a linear logical framework implemented within the Hybrid system. Hybrid is designed to support the use of higher-order abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic, which provides infrastructure for reasoning directly about object languages with linear features. We developed this framework in order to address the chal- lenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the Proto-Quipper language, which contains the core of Quipper. Quipper is a new quantum programming lan- guage under active development with a linear type system. We have completed a formal proof of type soundness for Proto-Quipper. Our current work includes extending this work to other properties of Proto-Quipper as well as reason- ing about other quantum programming languages. It also includes reasoning about other object languages with linear features in areas such as meta-theory of low-level abstract machine code, proof theory of focused linear sequent calculi, and modeling biological processes as transition systems and proving properties about them.

Mon 14 Jan
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

09:00 - 10:30: CPP 2019 - Keynote 1 and Research Paper at Sala XII
Chair(s): Magnus O. MyreenChalmers University of Technology, Sweden
CPP-201909:00 - 10:00
Amy FeltyUniversity of Ottawa
CPP-201910:00 - 10:30
Research paper
Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA