Electronic Appendix

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic, by Mohamed Yousri Mahmoud and Amy P. Felty, Journal of Automated Reasoning, June 2019, to appear.

The files run in Coq V8.9.0 They must be compiled in the order they appear below.

ProtoQuipperTypes.v
Hybrid.v
ProtoQuipperSyntax.v
LSL.v
ProtoQuipperProg.v
PQAdequacy.v
ProgLemmas1.v
ProgLemmas2.v
ProgLemmas3.v
SubjectReduction.v
SRCorollary.v

The code is also is available as a zip file.

ProtoQuipperFormalization.zip