A Linear Logical Framework in Hybrid (Invited Talk)

Author Amy P. Felty

Thumbnail PDF


  • Filesize: 208 kB
  • 2 pages

Document Identifiers

Author Details

Amy P. Felty
  • University of Ottawa, Canada

Cite AsGet BibTex

Amy P. Felty. A Linear Logical Framework in Hybrid (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • 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
  • Logical frameworks
  • proof assistants
  • linear logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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.
  6. Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, August 2015. URL: http://arxiv.org/abs/1510.02198.
  7. 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. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail