A Linear Logical Framework in Hybrid
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:00|
Amy FeltyUniversity of OttawaDOI
|10:00 - 10:30|
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky MachinesDOI