arXiv subjects

Matteo Cimini

Publications and source records attributed to Matteo Cimini.

12 recordsLinked to original sources

arXiv2026

A Typestate Approach to Purpose-aware Programming

Real-world applications often require verification that sensitive data is being used for their intended purpose. However, existing literature offers limited results regarding compile-time guarantees in this domain. In this paper, we explore the use of typestate to reason about the purpose of data. In typestate, types have a state, which can transition to other states in the style of automata. In our approach, the state of the type of sensitive data is defined as the set of purposes for which the data can be used. This set can grow or shrink at runtime as purposes can be added or removed during execution. In this paper, we have developed PurPL, an object-oriented programming language that features a typestate system that is capable of reasoning about purposes and data usage compliance according to them. We give an overview of PurPL through examples and present a formal type system. We have also implemented PurPL's type checker, and we report on our experiments with type checking various programming scenarios that handle sensitive data.

cs.PL↗

arXiv2024

From Program Logics to Language Logics

Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of the form $\{P\}\ \mathcal{X}\ \{Q\}$ where $\mathcal{X}$, the subject of analysis, can be a language component such as a piece of grammar, a typing rule, a reduction rule or other parts of a language definition. To demonstrate our approach, we develop $\mathbb{L}$, a language logic that can be used to analyze language definitions on various aspects of language design. We illustrate $\mathbb{L}$ to the analysis of some selected aspects of a programming language. We have also implemented an automated prover for $\mathbb{L}$, and we confirm that the tool repeats these analyses. Ultimately, $\mathbb{L}$ cannot verify languages. Nonetheless, we believe that this paper provides a strong first step towards adopting the methods of program logics for the analysis of languages.

cs.PL↗

arXiv2023

A Declarative Validator for GSOS Languages

Rule formats can quickly establish meta-theoretic properties of process algebras. It is then desirable to identify domain-specific languages (DSLs) that can easily express rule formats. In prior work, we have developed Lang-n-Change, a DSL that includes convenient features for browsing language definitions and retrieving information from them. In this paper, we use Lang-n-Change to write a validator for the GSOS rule format, and we augment Lang-n-Change with suitable macros on our way to do so. Our GSOS validator is concise, and amounts to a few lines of code. We have used it to validate several concurrency operators as adhering to the GSOS format. Moreover, our code expresses the restrictions of the format declaratively.

cs.PL↗

arXiv2022

Lang-n-Send Extended: Sending Regular Expressions to Monitors

In prior work, Cimini has presented Lang-n-Send, a pi-calculus with language definitions. In this paper, we present an extension of this calculus called Lang-n-Send+m. First, we revise Lang-n-Send to work with transition system specifications rather than its language specifications. This revision allows the use of negative premises in deduction rules. Next, we extend Lang-n-Send with monitors and with the ability of sending and receiving regular expressions, which then can be used in the context of larger regular expressions to monitor the execution of programs. We present a reduction semantics for Lang-n-Send+m, and we offer examples that demonstrate the scenarios that our calculus captures.

cs.PL↗

arXiv2022

Lang-n-Send: Processes That Send Languages

We present Lang-n-Send, a pi-calculus that is equipped with language definitions. Processes can define languages in operational semantics, and use them to execute programs. Furthermore, processes can send and receive pieces of operational semantics through channels. We present a reduction semantics for Lang-n-Send, and we offer examples that demonstrate some of the scenarios that Lang-n-Send captures.

cs.PL↗

arXiv2021

Language Transformations in the Classroom

Language transformations are algorithms that take a language specification in input, and return the language specification modified. Language transformations are useful for automatically adding features such as subtyping to programming languages (PLs), and for automatically deriving abstract machines. In this paper, we set forth the thesis that teaching programming languages features with the help of language transformations, in addition to the planned material, can be beneficial for students to help them deepen their understanding of the features being taught. We have conducted a study on integrating language transformations into an undergraduate PL course. We describe our study, the material that we have taught, and the exam submitted to students, and we present the results from this study. Although we refrain from drawing general conclusions on the effectiveness of language transformations, this paper offers encouraging data. We also offer this paper to inspire similar studies.

cs.PL↗

arXiv2020

Passive flow-separation control in a dual-bell rocket nozzle

A delayed detached eddy simulation of a sub-scale cold-gas dual-bell nozzle flow at high Reynolds number and in sea-level mode is carried out at nozzle pressure ratio NPR=45.7. In this regime the over-expanded flow exhibits a symmetric and controlled flow separation at the inflection point, that is the junction between the two bells, leading to the generation of a low content of aerodynamic side loads with respect to conventional bell nozzles. The nozzle wall-pressure signature is analysed in the frequency domain and compared with the experimental data available in the literature for the same geometry and flow conditions. The Fourier spectra in time and space (azimuthal wavenumber) show the presence of a persistent tone associated to the symmetric shock movement. Asymmetric modes are only slightly excited by the shock and the turbulent structures. The low mean value of the side-loads magnitude is in good agreement with the experiments and confirms that the inflection point dampens the aero-acoustic interaction between the separation-shock and the detached shear layer.

physics.flu-dyn↗

arXiv2019

A Calculus for Language Transformations

In this paper we propose a calculus for expressing algorithms for programming languages transformations. We present the type system and operational semantics of the calculus, and we prove that it is type sound. We have implemented our calculus, and we demonstrate its applicability with common examples in programming languages. As our calculus manipulates inference systems, our work can, in principle, be applied to logical systems.

cs.PL↗

arXiv2019

Towards Gradually Typed Capabilities in the Pi-Calculus

Gradual typing is an approach to integrating static and dynamic typing within the same language, and puts the programmer in control of which regions of code are type checked at compile-time and which are type checked at run-time. In this paper, we focus on the pi-calculus equipped with types for the modeling of input-output capabilities of channels. We present our preliminary work towards a gradually typed version of this calculus. We present a type system, a cast insertion procedure that automatically inserts run-time checks, and an operational semantics of a pi-calculus that handles casts on channels. Although we do not claim any theoretical results on our formulations, we demonstrate our calculus with an example and discuss our future plans.

cs.PL↗

arXiv2016

Well-Typed Languages are Sound

Type soundness is an important property of modern programming languages. In this paper we explore the idea that "well-typed languages are sound": the idea that the appropriate typing discipline over language specifications guarantees that the language is type sound. We instantiate this idea for a certain class of languages defined using small step operational semantics by ensuring the progress and preservation theorems. Our first contribution is a syntactic discipline for organizing and restricting language specifications so that they automatically satisfy the progress theorem. This discipline is not novel but makes explicit the way expert language designers have been organizing a certain class of languages for long time. We give a formal account of this discipline by representing language specifications as (higher-order) logic programs and by giving a meta type system over that collection of formulas. Our second contribution is a methodology and meta type system for guaranteeing that languages satisfy the preservation theorem. Ultimately, we proved that language specifications that conform to our meta type systems are guaranteed to be type sound. We have implemented these ideas in the TypeSoundnessCertifier, a tool that takes language specifications in the form of logic programs and type checks them according to our meta type systems. For those languages that pass our type checker, our tool automatically produces a proof of type soundness that can be machine-checked by the Abella proof assistant. For those languages that fail our type checker, the tool pinpoints the design mistakes that hinder type soundness. We have applied the TypeSoundnessCertifier to a large number of programming languages, including those with recursive types, polymorphism, letrec, exceptions, lists and other common types and operators.

cs.PL↗

arXiv2011

Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca

In this paper we propose an extension of the Rebeca language that can be used to model distributed and asynchronous systems with timing constraints. We provide the formal semantics of the language using Structural Operational Semantics, and show its expressiveness by means of examples. We developed a tool for automated translation from timed Rebeca to the Erlang language, which provides a first implementation of timed Rebeca. We can use the tool to set the parameters of timed Rebeca models, which represent the environment and component variables, and use McErlang to run multiple simulations for different settings. Timed Rebeca restricts the modeller to a pure asynchronous actor-based paradigm, where the structure of the model represents the service oriented architecture, while the computational model matches the network infrastructure. Simulation is shown to be an effective analysis support, specially where model checking faces almost immediate state explosion in an asynchronous setting.

cs.SE↗

arXiv2010

A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages

This paper presents a bisimulation-based method for establishing the soundness of equations between terms constructed using operations whose semantics is specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de Simone's FH-bisimilarity and uses transition rules as schematic transitions in a bisimulation-like relation between open terms. The soundness of the method is proven and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but the article offers some completeness results for restricted classes of GSOS specifications.

cs.LO↗