On Circuit Description Languages, Indexed Monads, and Resource Analysis
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917110273277952 |
|---|---|
| author | Sakayori, Ken Colledan, Andrea Lago, Ugo Dal |
| author_facet | Sakayori, Ken Colledan, Andrea Lago, Ugo Dal |
| contents | In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_22419 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Circuit Description Languages, Indexed Monads, and Resource Analysis Sakayori, Ken Colledan, Andrea Lago, Ugo Dal Programming Languages In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations. |
| title | On Circuit Description Languages, Indexed Monads, and Resource Analysis |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2511.22419 |