Semantic typing has become a powerful tool for program verification, applying the technique of logical relations as not only a proof method, but also a device for prescribing program behavior. In recent work, Yao et al. scaled semantic typing to the verification of timed message-passing protocols, which are prevalent in, e.g., IoT and real-time systems applications. The appeal of semantic typing in this context is precisely because of its ability to support typed and untyped program components alike – including physical objects – which caters to the heterogeneity of these applications. Another demand inherent to these applications is timing: constraining the time or time window within which a message exchange must happen. Yao et al. equipped their logical relation not only with temporal predicates, but also with computable trajectories, to supply the evidence that an inhabitant can step from one time point to another one. While Yao et al. provide the formalization for such a verification tool, it lacks a mechanization. Mechanizing the system would not only provide a machine proof for it, but also facilitate scalability for future extensions and applications. This paper tackles the challenge of mechanizing the resulting proof-relevant logical relation in a proof assistant. allowing trajectories to be interleaved, partitioned, and concatenated, while the intended equality on trajectories is the equality of their graphs when seen as processes indexed by time. Unfortunately, proof assistants based on intensional type theory only have modest support for such equations, forcing a prolific use of transports. This paper reports on the process of mechanizing Yao et al.‘s results, comprising the logical relation, the algebra of computable trajectories with supporting lemmas, and the fundamental theorem of the logical relation, in the Rocq theorem prover.

Today’s computing landscape has been gradually shifting to applications targeting distributed and heterogeneous systems, such as cloud computing and Internet of Things (IoT) applications. These applications are predominantly concurrent, employ message-passing, and interface with foreign objects, ranging from externally implemented code to actual physical devices such as sensors. Verifying that the resulting systems adhere to the intended protocol of interaction is challenging – the usual assumption of a common implementation language, let alone a type system, no longer applies, ruling out any verification method based on them. This paper develops a framework for certifying protocol compliance of heterogeneous message-passing systems. It contributes the first mechanization of a language-agnostic logical relation, asserting that its inhabitants comply with the protocol specified. This definition relies entirely on a labelled transition-based semantics, accommodating arbitrary inhabitants, typed and untyped alike, including foreign objects. As a case study, the paper considers two scenarios: (1) per-instance verification of a specific application or hardware device, and (2) once-and-for-all verification of well-typed applications for a given type system. The logical relation and both scenarios are mechanized in the Coq theorem prover.

Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.

We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define parametric subtyping , a conceptually simple, decidable, and expressive fragment of structural subtyping that strictly generalizes rigid subtyping . We present and prove correct an effective saturation-based decision procedure for parametric subtyping, demonstrating its applicability using a variety of examples. We also provide an implementation of this decision procedure as an artifact.

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts , which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian’s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian’s type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.

Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.