arXiv subjects

Paolo Torrini

Publications and source records attributed to Paolo Torrini.

5 recordsLinked to original sources

arXiv2025

KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM

High-assurance cryptography provides strong guarantees that source implementations are functionally correct and provably secure. In this paper, we demonstrate that the Jasmin compiler preserves functional correctness and KEM-IND-CCA security (which were established in prior work) of a highly optimized Jasmin implementation of ML-KEM used in the popular messenger Signal. Our proof of preservation is fully mechanized in the Rocq prover and is based on three general contributions: (1) A general framework for modeling game-based security and for reasoning about preservation of game-based security under compilation. (2) A new, interaction-trees-based semantics of Jasmin and assembly programs. Our new semantics supports features required by ML-KEM, such as probabilistic computations and rejection sampling routines. (3) A new relational Hoare logic for interaction trees, which we use to prove correctness of the JASMIN compiler under our new semantics.

cs.PL↗

arXiv2016

A Modular Structural Operational Semantics for Delimited Continuations

It has been an open question as to whether the Modular Structural Operational Semantics framework can express the dynamic semantics of call/cc. This paper shows that it can, and furthermore, demonstrates that it can express the more general delimited control operators control and shift.

cs.PL↗

arXiv2015

Reasoning about modular datatypes with Mendler induction

In functional programming, datatypes a la carte provide a convenient modular representation of recursive datatypes, based on their initial algebra semantics. Unfortunately it is highly challenging to implement this technique in proof assistants that are based on type theory, like Coq. The reason is that it involves type definitions, such as those of type-level fixpoint operators, that are not strictly positive. The known work-around of impredicative encodings is problematic, insofar as it impedes conventional inductive reasoning. Weak induction principles can be used instead, but they considerably complicate proofs. This paper proposes a novel and simpler technique to reason inductively about impredicative encodings, based on Mendler-style induction. This technique involves dispensing with dependent induction, ensuring that datatypes can be lifted to predicates and relying on relational formulations. A case study on proving subject reduction for structural operational semantics illustrates that the approach enables modular proofs, and that these proofs are essentially similar to conventional ones.

cs.LO↗

arXiv2010

Resource-Bound Quantification for Graph Transformation

Graph transformation has been used to model concurrent systems in software engineering, as well as in biochemistry and life sciences. The application of a transformation rule can be characterised algebraically as construction of a double-pushout (DPO) diagram in the category of graphs. We show how intuitionistic linear logic can be extended with resource-bound quantification, allowing for an implicit handling of the DPO conditions, and how resource logic can be used to reason about graph transformation systems.

cs.LO↗

arXiv2009

Towards an embedding of Graph Transformation in Intuitionistic Linear Logic

Linear logics have been shown to be able to embed both rewriting-based approaches and process calculi in a single, declarative framework. In this paper we are exploring the embedding of double-pushout graph transformations into quantified linear logic, leading to a Curry-Howard style isomorphism between graphs and transformations on one hand, formulas and proof terms on the other. With linear implication representing rules and reachability of graphs, and the tensor modelling parallel composition of graphs and transformations, we obtain a language able to encode graph transformation systems and their computations as well as reason about their properties.

cs.LO↗