2026-07-22T11:26:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17100 2024-03-06T10:58:45Z ddc:004 open_access

On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments Dal Lago, Ugo Giusti, Giulia Session Types Probabilistic Computation Bounded Linear Logic Cryptographic Experiments 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ugo Dal Lago and Giulia Giusti 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.37 urn:nbn:de:0030-drops-171000 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.37 eng https://creativecommons.org/licenses/by/4.0/legalcode