A Linear Logical Framework in Hybrid (Invited Talk)
We present a linear logical framework implemented within the Hybrid system [Amy P. Felty and Alberto Momigliano, 2012]. 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 two linear specification logics, which provide infrastructure for reasoning directly about object languages with linear features.
We originally developed this framework in order to address the challenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the Proto-Quipper language [Neil J. Ross, 2015], which contains the core of Quipper [Green et al., 2013; Peter Selinger and Benoît Valiron, 2006]. Quipper is a relatively new quantum programming language under active development with a linear type system. We have completed a formal proof of type soundness for Proto-Quipper [Mohamed Yousri Mahmoud and Amy P. Felty, 2018]. Our current work includes extending this work to other properties of Proto-Quipper, reasoning about other quantum programming languages [Mohamed Yousri Mahmoud and Amy P. Felty, 2018], and reasoning about other languages such as the meta-theory of low-level abstract machine code.
We are also interested in applying this framework to applications outside the domain of meta-theory of programming languages and have focused on two areas - formal reasoning about the proof theory of focused linear sequent calculi and modeling biological processes as transition systems and proving properties about them. We found that a slight extension of the initial linear specification logic allowed us to provide succinct encodings and facilitate reasoning in these new domains. We illustrate by discussing a model of breast cancer progression as a set of transition rules and proving properties about this model [Joëlle Despeyroux et al., 2018]. Current work also includes modeling stem cells as they mature into different types of blood cells.
This work illustrates the use of Hybrid as a meta-logical framework for fast prototyping of logical frameworks, which is achieved by defining inference rules of a specification logic inductively in Coq and building a library of definitions and lemmas used to reason about a class of object logics. Our focus here is on linear specification logics and their applications.
Logical frameworks
proof assistants
linear logic
Theory of computation~Logic and verification
Theory of computation~Operational semantics
Theory of computation~Type theory
Theory of computation~Functional constructs
Theory of computation~Type structures
2:1-2:2
Invited Talk
Amy P.
Felty
Amy P. Felty
University of Ottawa, Canada
http://www.site.uottawa.ca/~afelty/
https://orcid.org/0000-0001-7195-2613
The author acknowledges the support of the Natural Sciences and Engineering Research Council of Canada.
10.4230/LIPIcs.FSCD.2019.2
Joëlle Despeyroux, Amy Felty, Pietro Lio, and Carlos Olarte. A Logical Framework for Modelling Breast Cancer Progression. In International Symposium on Molecular Logic and Computational Synthetic Biology (MLCSB), 2018.
Amy P. Felty and Alberto Momigliano. Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax. Journal of Automated Reasoning, 48(1):43-105, 2012.
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A Scalable Quantum Programming Language. In Thirty-Fourthh ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 333-342. ACM, 2013.
Mohamed Yousri Mahmoud and Amy P. Felty. Formal Meta-level Analysis Framework for Quantum Programming Languages. In 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017), volume 338 of Electronic Notes in Theoretical Computer Science, pages 185-201, 2018.
Mohamed Yousri Mahmoud and Amy P. Felty. Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. CoRR, 2018. URL: http://arxiv.org/abs/1812.03624.
http://arxiv.org/abs/1812.03624
Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, August 2015. URL: http://arxiv.org/abs/1510.02198.
http://arxiv.org/abs/1510.02198
Peter Selinger and Benoît Valiron. A Lambda Calculus for Quantum Computation with Classial Control. Mathematical Structures in Computer Science, 16(3):527-552, 2006.
Amy P. Felty
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode