Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of Quipper. Quipper is a quantum programming language under active development and recently has gained much popularity among the quantum computing communities. Hybrid is a system that 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 (SL) in order to reason about the linear type system of Quipper. To this end, we formalize the semantics of Proto-Quipper by encoding the typing and evaluation rules in the SL, and prove type soundness.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. In general, when we stray from the original presentation, our intention is to simplify formalization, and we only do so when there is a clear equivalence to the original. In this case, we simplify the formalization of the subtyping relation without changing the semantics of types. As we will discuss in the next section, making this kind of change also led to the discovery of a small mistake in the original presentation.

  2. This is straightforward change, but it affects a large portion of the proof development and is left for (very near) future work.

  3. We also impose the restriction that the Coq derivation must be minimal in the same sense as described there. See [13] for details.

  4. A variety of other internal adequacy lemmas are shown in [14].

References

  1. Altenkirch, T., Grattage, J.: A functional quantum programming language. In: Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, pp. 249–258 (2005)

  2. Ambler, S., Crole, R.L., Momigliano, A.: Combining higher order abstract syntax with tactical theorem proving and (co)induction. In :15th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs). Lecture Notes in Computer Science. Springer, pp. 13–30 (2002)

  3. Battell, C., Felty, A.: The logic of hereditary Harrop formulas as a specification logic for Hybrid. In: Proceedings of the 11th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2011). ACM, pp. 3:1–3:10 (2016)

  4. Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19–75 (2002)

    Article  MathSciNet  Google Scholar 

  5. Crole, R.L.: The representational adequacy of Hybrid. Math. Struct. Comput. Sci. 21(3), 585–646 (2011)

    Article  MathSciNet  Google Scholar 

  6. Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Second International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science. Springer, pp. 124–138 (1995)

  7. Dal Lago, U., Masini, A., Zorzi, M.: On a measurement-free quantum lambda calculus with classical control. Math. Struct. Comput. Sci. 19(2), 297–335 (2009)

    Article  MathSciNet  Google Scholar 

  8. Dal Lago, U., Masini, A., Zorzi, M.: Quantum implicit computational complexity. Theor. Comput. Sci. 411(2), 377–409 (2010)

    Article  MathSciNet  Google Scholar 

  9. Felty, A., et al.: Two-level hybrid: a system for reasoning using higher-order abstract syntax. http://www.site.uottawa.ca/~afelty/HybridCoq/ 2019. Accessed 14 May 2019

  10. Felty, A., Momigliano, A.: Reasoning with hypothetical judgments and open terms in Hybrid. In: Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011). ACM, pp. 83–92 (2011)

  11. Felty, A., Momigliano, A., Pientka, B.: An open challenge problem repository for systems supporting binders. In: Proceedings of the 10th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP 2015), Volume 185 of Electronic Proceedings in Theoretical Computer Science, pp. 18–32 (2015)

    Article  MathSciNet  Google Scholar 

  12. Felty, A., Momigliano, A., Pientka, B.: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. Comput. Sci. 1–34 (2017)

  13. Felty, A.P., Momigliano, A.: Hybrid: a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. 48(1), 43–105 (2012)

    Article  Google Scholar 

  14. Felty, A.P., Momigliano, A., Pientka, B.: The next 700 challenge problems for reasoning with higher-order abstract syntax representations: part 2—a survey. J. Autom. Reason. 55(4), 307–372 (2015)

    Article  MathSciNet  Google Scholar 

  15. Gacek, A.: The Abella interactive theorem prover (system description). In: Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Volume 5195 of Lecture Notes in Computer Science. Springer, pp. 154–161 (2008)

  16. Grattage, J.: An overview of QML with a concrete implementation in Haskell. Electron. Notes Theor. Comput. Sci. 270(1), 165–174 (2011)

    Article  Google Scholar 

  17. Green, A.S., LeFanu L., Peter, R., Neil, J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Thirty-Fourth ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, pp. 333–342 (2013)

  18. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143–184 (1993)

    Article  MathSciNet  Google Scholar 

  19. Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110(2), 327–365 (1994)

    Article  MathSciNet  Google Scholar 

  20. Lindenhovius, B., Mislove, M., Zamdzhiev, V.: Enriching a linear/non-linear lambda calculus: a programming language for string diagrams. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM, pp. 659–668 (2018)

  21. Mahmoud, M.Y., Felty, A.P.: Formalization of metatheory of the Quipper quantum programming language in a linear logic: Coq script. http://www.site.uottawa.ca/~afelty/jar19. Accessed 18 June 2019

  22. Mahmoud, M.Y., Felty, A.P.: Formal meta-level analysis framework for quantum programming languages. In: 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017), Electronic Notes in Theoretical Computer Science, 338, 185–201 (2018)

    Article  MathSciNet  Google Scholar 

  23. Martin, A.J.: Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study. PhD thesis, University of Ottawa (2010)

  24. Martin, A.J., Felty, A.P.: An improved implementation and abstract interface for Hybrid. In: Proceedings of the 6th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, (LFMTP 2011), Volume 71 of Electronic Proceedings in Theoretical Computer Science, pp. 76–90 (2011)

    Article  Google Scholar 

  25. McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. 3(1), 80–136 (2002)

    Article  MathSciNet  Google Scholar 

  26. Miller, D.: Forum: a multiple-conclusion specification logic. Theor. Comput. Sci. 165(1), 201–232 (1996)

    Article  MathSciNet  Google Scholar 

  27. Miller, D.: Overview of linear logic programming. In: Ehrhard, T., Girard, J.-Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science. London Mathematical Society Lecture Notes, vol. 316, pp. 119–150. Cambridge University Press, Cambridge (2004)

    Chapter  Google Scholar 

  28. Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)

    Book  Google Scholar 

  29. Miller, D., Palamidessi, C.: Foundational aspects of syntax. ACM Comput. Surv. 31(3es), 1–6 (1999)

    Article  Google Scholar 

  30. Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp. 199–208 (1988)

  31. Pientka, B.: Proof pearl: the power of higher-order encodings in the logical framework LF. In: Proceedings of the 20th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2007). Lecture Notes in Computer Science. Springer, pp. 246–261 (2007)

  32. Pientka, P., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Volume 6173 of Lecture Notes in Computer Science. Springer, pp. 15–21 (2010)

  33. Polakow, J.: Ordered Linear Logic and Applications. PhD thesis, Carnegie Mellon University (2001)

  34. Rand, R., Paykin, J., Zdancewic, S.: QWIRE practice: formal verification of quantum circuits in Coq. In : Postproceedings of the 14th International Conference on Quantum Physics and Logic (QPL 2017), Volume 266 of Electronic Proceedings in Theoretical Computer Science, pp. 119–132 (2018)

    Article  Google Scholar 

  35. Rios, F., Selinger, P.: A categorical model for a quantum circuit description language. In: Postproceedings of the 14th International Conference on Quantum Physics and Logic (QPL 2017), Volume 266 of Electronic Proceedings in Theoretical Computer Science, pp. 164–178 (2018). arXiv preprint arXiv:1706.02630

  36. Ross, N.J.: Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, August (2015). arXiv:1510.02198 [quant-ph]

  37. Selinger, P.: Personal communication, January (2016)

  38. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classial control. Math. Struct. Comput. Sci. 16(3), 527–552 (2006)

    Article  Google Scholar 

  39. Smith, R.S., Curtis, M.J., Zeng, W.J.: A practical quantum instruction set architecture (2017). arXiv:1608.03355v2 [quant-ph]

  40. Svore, K.M., Geller, A., Troyer, M., Azariah, J., Granade, C., Heim, B., Kliuchnikov, V., Mykhailova, M., Paz, A., Roetteler, M.: Q#: enabling scalable quantum computing and development with a high-level domain-specific language (2018). arXiv:1803.00652 [quant-ph]

  41. The Twelf Project. Introduction to Twelf: proving metatheorems about the STLC. http://twelf.org/wiki/Proving_metatheorems:Proving_metatheorems_about_the_STLC, 2009. Accessed 1 Oct 2016

  42. Wang, Y., Chaudhuri, K., Gacek, A., Nadathur, G.: Reasoning about higher-order relational specifications. In: Proceedings of the 15th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP). ACM, pp. 157–168 (2013)

  43. Zorzi, M.: On quantum lambda calculi: a foundational perspective. Math. Struct. Comput. Sci. 26(7), 1107–1195 (2016)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

The authors acknowledge the support of the Natural Sciences and Engineering Research Council of Canada. We would also like to thank the reviewers for their comments, which helped us to improve the paper. In addition, we would like to thank Julien Ross and Peter Selinger for useful discussions on technical details as well as on approaches and directions for this work. Finally, the second author would also like to extend her gratitude to the University of Ottawa’s Writers Retreats.

Author information

Authors and Affiliations

  1. School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, Canada

    Mohamed Yousri Mahmoud & Amy P. Felty

Authors
  1. Mohamed Yousri Mahmoud
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amy P. Felty
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Amy P. Felty.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Mahmoud, M.Y., Felty, A.P. Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. J Autom Reasoning 63, 967–1002 (2019). https://doi.org/10.1007/s10817-019-09527-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-019-09527-x

Keywords

Search

Navigation