-
From Program Logics to Language Logics
Authors:
Matteo Cimini
Abstract:
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 reduc…
▽ More
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.
△ Less
Submitted 2 August, 2024;
originally announced August 2024.
-
A Declarative Validator for GSOS Languages
Authors:
Matteo Cimini
Abstract:
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 valid…
▽ More
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.
△ Less
Submitted 13 April, 2023;
originally announced April 2023.
-
Lang-n-Send Extended: Sending Regular Expressions to Monitors
Authors:
Matteo Cimini
Abstract:
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…
▽ More
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.
△ Less
Submitted 9 August, 2022;
originally announced August 2022.
-
Lang-n-Send: Processes That Send Languages
Authors:
Matteo Cimini
Abstract:
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…
▽ More
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.
△ Less
Submitted 24 March, 2022;
originally announced March 2022.
-
Language Transformations in the Classroom
Authors:
Matteo Cimini,
Benjamin Mourad
Abstract:
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…
▽ More
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.
△ Less
Submitted 23 August, 2021;
originally announced August 2021.
-
A Calculus for Language Transformations
Authors:
Benjamin Mourad,
Matteo Cimini
Abstract:
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 princip…
▽ More
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.
△ Less
Submitted 25 October, 2019;
originally announced October 2019.
-
Towards Gradually Typed Capabilities in the Pi-Calculus
Authors:
Matteo Cimini
Abstract:
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 gra…
▽ More
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.
△ Less
Submitted 12 September, 2019;
originally announced September 2019.
-
Well-Typed Languages are Sound
Authors:
Matteo Cimini,
Dale Miller,
Jeremy G. Siek
Abstract:
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…
▽ More
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.
△ Less
Submitted 15 November, 2016;
originally announced November 2016.
-
Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca
Authors:
Luca Aceto,
Matteo Cimini,
Anna Ingolfsdottir,
Arni Hermann Reynisson,
Steinar Hugi Sigurdarson,
Marjan Sirjani
Abstract:
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 im…
▽ More
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.
△ Less
Submitted 31 July, 2011;
originally announced August 2011.
-
A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages
Authors:
Luca Aceto,
Matteo Cimini,
Anna Ingolfsdottir
Abstract:
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…
▽ More
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.
△ Less
Submitted 15 February, 2010;
originally announced February 2010.
