natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
algebraic quantum field theory (perturbative, on curved spacetimes, homotopical)
quantum mechanical system, quantum probability
interacting field quantization
Quipper is a functional quantum programming language
Resources:
Original articles:
Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48(6):333-342, 2013 (arXiv:1304.3390)
Jonathan Smith, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: Concrete Resource Estimation in Quantum Algorithms, QAPL 2014 (arXiv:1412.0625)
Review:
Further developments:
On dependent linear type theory with Quipper:
On quantum software verification for/with Quipper:
Last revised on February 16, 2021 at 23:50:54. See the history of this page for a list of all contributions to it.