License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2022.37
URN: urn:nbn:de:0030-drops-171000
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17100/
Dal Lago, Ugo ;
Giusti, Giulia
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments
Abstract
A system of session types is introduced as induced by a Curry Howard correspondence applied to bounded linear logic, suitably extended with probabilistic choice operators and ground types. The resulting system satisfies some expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.
BibTeX - Entry
@InProceedings{dallago_et_al:LIPIcs.CONCUR.2022.37,
author = {Dal Lago, Ugo and Giusti, Giulia},
title = {{On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {37:1--37:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/17100},
URN = {urn:nbn:de:0030-drops-171000},
doi = {10.4230/LIPIcs.CONCUR.2022.37},
annote = {Keywords: Session Types, Probabilistic Computation, Bounded Linear Logic, Cryptographic Experiments}
}
|
Keywords: |
|
Session Types, Probabilistic Computation, Bounded Linear Logic, Cryptographic Experiments |
|
Collection: |
|
33rd International Conference on Concurrency Theory (CONCUR 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
06.09.2022 |
