Smart contracts have played a pivotal role in the evolution of blockchains and Decentralized Applications (DApps). As DApps continue to gain widespread adoption, multiple smart contract languages have been and are being made available to developers, each with its distinctive features, strengths, and weaknesses. In this paper, we examine the smart contract languages used in major blockchain platforms, with the goal of providing a comprehensive assessment of their main properties. Our analysis targets the programming languages rather than the underlying architecture: as a result, while we do consider the interplay between language design and blockchain model, our main focus remains on language-specific features such as usability, programming style, safety and security. To conduct our assessment, we propose an original benchmark which encompasses a wide, yet manageable, spectrum of key use cases that cut across all the smart contract languages under examination. • We give an abstract overview of smart contract platforms, discussing the impact of different design choices. • We illustrate by examples how different design choices give rise to different programming styles for smart contracts. • We consider 6 leading smart contract languages: Solidity (Ethereum), Rust (Solana), Aiken (Cardano), PyTeal (Algorand), Move (Aptos), SmartPy (Tezos). • We develop an open-source benchmark of use cases of smart contracts, implemented in all the languages in our selection. • Based on our benchmark, we evaluate smart contract languages focussing on their security, code readability, usability, and functionalities.

We present Stipula, a domain specific language that may assist legal practitioners in programming legal contracts through specific patterns. The language is based on a small set of programming abstractions that correspond to common patterns in legal contracts. We illustrate the language by means of two paradigmatic legal contracts: a bike rental and a bet contract. Stipula comes with a formal semantics, an observational equivalence and a type inference system, that provide for a clear account of the contracts' behaviour and illustrate how several concepts from concurrency theory can be adapted to automatically verify the properties and the correctness of software-based legal contracts. We also discuss a prototype centralized implementation of Stipula.

We study the proof theory and the automatic proof search for a fragment of linear logic with context-sensitive deductions inspired by molecular biology. We formulate an intuitionistic (multiplicative) linear logic sequent calculus where sequents are decorated so to account for the biological constraints. We then draw on the literature to develop a generalized proof search technique that allows to automatically deal with context-sensitive deductions and non-monotonic reasoning. Finally, we present the implementation of a theorem prover that can be used to automatically verify biological pathways expressed as logical sequents.

We introduce a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations on objects are molecules of messages, and state transformations are chemical reactions. This approach allows us to investigate typestate in an inherently concurrent setting, whereby objects can be accessed and modified concurrently by several processes, each potentially changing only part of their state. We introduce a simple behavioral type theory to express in a uniform way both the private and the public interfaces of objects; describe and enforce structured object protocols consisting of possibilities, prohibitions, and obligations; and control object sharing.

We study a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations on objects are molecules of messages and state transformations are chemical reactions. This approach allows us to investigate typestate in an inherently concurrent setting, whereby objects can be accessed and modified concurrently by several processes, each potentially changing only part of their state. We introduce a simple behavioral type theory to express in a uniform way both the private and the public interfaces of objects, to describe and enforce structured object protocols consisting of possibilities, prohibitions, and obligations, and to control object sharing.

We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history-preserving bisimilarity, and fragments of the logic can be identified which correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history-preserving bisimilarity. Standard Hennessy-Milner logic, and thus (interleaving) bisimilarity, is also recovered as a fragment. We also propose an extension of the logic with fixpoint operators, thus allowing to describe causal and concurrency properties of infinite computations. This work contributes to a rational presentation of the true concurrent spectrum and to a deeper understanding of the relations between the involved behavioural equivalences.

Probabilistic nondeterministic processes are commonly modeled as probabilistic LTSs (PLTSs). A number of logical characterizations of the main behavioral relations on PLTSs have been studied. In particular, Parma and Segala [2007] and Hermanns et al. [2011] define a probabilistic Hennessy-Milner logic interpreted over probability distributions, whose corresponding logical equivalence/preorder when restricted to Dirac distributions coincides with standard bisimulation/simulation between the states of a PLTS. This result is here extended by studying the full logical equivalence/preorder between (possibly non-Dirac) distributions in terms of a notion of bisimulation/simulation defined on an LTS whose states are distributions (dLTS). We show that the well-known spectrum of behavioral relations on nonprobabilistic LTSs as well as their corresponding logical characterizations in terms of Hennessy-Milner logic scales to the probabilistic setting when considering dLTSs.

A number of algorithms for computing the simulation preorder on Kripke structures and on labelled transition systems are available. Among them, the algorithm by Ranzato and Tapparo [2007] has the best time complexity,while the algorithm by Gentilini

Discretionary Access Control (DAC) systems provide powerful resource management mechanisms based on the selective distribution of capabilities to selected classes of principals. We study a type-based theory of DAC models for a process calculus that extends Cardelli, Ghelli and Gordon's pi-calculus with groups (Cardelliet al. 2005). In our theory, groups play the role of principals and form the unit of abstraction for our access control policies, and types allow the specification of fine-grained access control policies to govern the transmission of names, bound the (iterated) re-transmission of capabilities and predicate their use on the inability to pass them to third parties. The type system relies on subtyping to achieve a selective distribution of capabilities to the groups that control the communication channels. We show that the typing and subtyping relationships of the calculus are decidable. We also prove a type safety result, showing that in well-typed processes all names: (i) flow according to the access control policies specified by their types; and (ii) are received at the intended sites with the intended capabilities. We illustrate the expressive power and the flexibility of the typing system using several examples.

Boxed Ambients are a variant of Mobile Ambients that result from dropping the open capability and introducing new primitives for ambient communication. The new model of communication is faithful to the principles of distribution and location-awareness of Mobile Ambients, and complements the constructs in and out for mobility with finer-grained mechanisms for ambient interaction. We introduce the new calculus, study the impact of the new mechanisms for communication of typing and mobility, and show that they yield an effective framework for resource protection and access control in distributed systems.

Finding typed encodings of object-oriented into procedural or functional programming sheds light on the theoretical foundations of object-oriented languages and their specific typing constructs and techniques. This article describes a type preserving and computationally adequate interpretation of a full-fledged object calculus that supports message passing and constructs for object update and extension. The target theory is a higher-order λ-calculus with records and recursive folds/unfolds, polymorphic and recursive types, and subtyping. The interpretation specializes to calculi of nonextensible objects, and validates the expected subtypin