2026-08-06T07:56:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18446 2024-03-06T11:01:51Z ddc:004 open_access

On Dynamic Lifting and Effect Typing in Circuit Description Languages Colledan, Andrea Dal Lago, Ugo Circuit-Description Languages λ-calculus Dynamic lifting Type and effect systems In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, which models the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrea Colledan and Ugo Dal Lago 2023 Is Part Of LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2022.3 urn:nbn:de:0030-drops-184468 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.3 eng https://creativecommons.org/licenses/by/4.0/legalcode