Ent: A Usable Quantum Programming Language on Top of the Enter Calculus

Résumé fourni par la source

Ent (source files .ent, compiler entc) is a surface language whose only semantics is to desugar to a closed Enter-calculus term and reduce it. Consequently, every theorem of the Enter calculus applies to every Ent program for free. The compiler also literally re-checks its own output by passing the emitted core term back to enter.typing_rules.typecheck.This document specifies the surface syntax, the staged compile-time and run-time type discipline, the complete desugaring into the core calculus, the compiler architecture, and a reference implementation in Python that extends the existing enter-calculus artefact package. Section 11 states precisely which guarantees are inherited from which theorem and which guarantees are not available. Appendix A provides a consolidated log of thirty corrections, identified as D1–D30, that were applied to the first draft of the implementation. The listings in Section 8 contain the corrected sources.