This paper introduces a new categorical structure that is a model of a variant of the i/o-typed pi-calculus, in the same way that a cartesian closed category is a model of the \lambda-calculus. To the best of our knowledge, no categorical model has been given for the i/o-typed pi-calculus, in contrast to session-typed calculi, to which corresponding logic and categorical structure were given. The categorical structure introduced in this paper has a simple definition, combining two well-known structures, namely, closed Freyd category and compact closed category. The former is a model of effectful computation in a general setting, and the latter describes connections via channels, which cause the effect we focus on in this paper. To demonstrate relevance of the categorical model, we show by a semantics consideration that the pi-calculus is equivalent to a core calculus of concurrent ML.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_23

Ken Sakayori

The University of Tokyo

Takeshi Tsukada

University of Tokyo, Japan

We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling the collision of data packets. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we also show that the version with virtual carrier sensing overcomes not only this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_24

Rob van Glabbeek

Peter Höfner

Michael Markl

We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework.

The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_27

Carsten Fuhs

Birkbeck, University of London

United Kingdom

Cynthia Kop

Radboud University Nijmegen

Netherlands

We present an abstract domain able to infer invariants on programs manipulating trees. Trees considered in the article are defined over a finite alphabet and can contain unbounded numeric values at their leaves. Our domain can infer the possible shapes of the tree values of each variable and find numeric relations between: the values at the leaves as well as the size and depth of the tree values of different variables. The abstract domain is described as a product of (1) a symbolic domain based on a tree automata representation and (2) a numerical domain lifted, for the occasion, to describe numerical maps with potentially infinite and heterogeneous definition set. In addition to abstract set operations and widening we define concrete and abstract transformers on these environments. We present possible applications, such as the ability to describe memory zones, or track symbolic equalities between program variables. We implemented our domain in a static analysis platform and present preliminary results analyzing a tree-manipulating toy-language.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_26

Matthieu Journault

Antoine Miné

UPMC, France

France

Abdelraouf Ouadjaout

Sorbonne Université

France

We present a behavioural typing system for a higher-order timed calculus, using types to model timed protocols (i.e., application-level specifications of interaction patterns among distributed applications), and the calculus to abstract implementations. Behavioural typing ensures that processes in the calculus will perform actions in the time-windows prescribed by their protocols. We introduce duality and subtyping relations for timed asynchronous session types. Duality includes a class of protocols that previous work on asynchronous timed session types could not type-check. Subtyping is critical for precision of our typing system, especially in the case of session delegation. The composition of dual timed asynchronous types enjoys progress when using an urgent receive semantics, in which receive actions are executed as soon as the expected message is available. Our calculus increases the modelling power of calculi used in the previous timed session work. Specifically, we add a blocking receive primitive with timeout, and a primitive that consumes an arbitrary amount of time in a given range.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_21

Laura Bocchi

University of Kent

United Kingdom

Maurizio Murgia

Vasco Thudichum Vasconcelos

Nobuko Yoshida

Imperial College London

Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codata for programming has been mainly relegated to representing infinite objects and processes. Our goal is to demonstrate the benefits of codata as a general-purpose programming abstraction independent of any specific language (i.e. with a specific evaluation strategy, typing discipline, paradigm, etc.). While codata is not featured in many programming languages today, we show how codata can be easily adopted and implemented by offering simple inter-compilation techniques between data and codata. Ultimately, we hope to utilize the Curry-Howard correspondence to find a common ground and bridge the gap between the functional and object-oriented paradigms.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_5

Paul Downen

University of Oregon, USA

Zachary Sullivan

Zena M. Ariola

University of Oregon, USA

Simon Peyton Jones

Microsoft, UK

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is recast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to novel coalgebraic interpretation of complete Herbrand models.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_28

Henning Basold

CNRS & ENS Lyon

Ekaterina Komendantskaya

Heriot-Watt University, UK

Yue Li

Heriot-Watt University, UK

China

Software Fault Isolation is a security-enhancing program transformation for instrumenting an untrusted binary module so that it runs inside a dedicated isolated address space, called a sandbox. To ensure that the untrusted module cannot escape its sandbox, existing approaches such as Google’s Native Client relies on a binary verifier to check that all memory accesses are within the sandbox. Instead of relying on a posteriori verification, Portable Software Fault Isolation proposes to insert a program instrumentation phase as part of a certified compiler, and leverage the soundness proof of this compiler to enforce a sandboxing security property. This eliminates the need for a binary verifier. In this paper, we describe the design, implementation and proof of an efficient, machine-checked \compcert implementation of Portable Software Fault Isolation. We propose a novel sandboxing transformation that has a well-defined C semantics and which supports arbitrary function pointers. Experiments show that our formally verified technique is a competitive way of implementing Software Fault Isolation.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_18

Frédéric Besson

Sandrine Blazy

Univ Rennes- IRISA

France

Alexandre Dang

Thomas P. Jensen

INRIA Rennes

Pierre Wilke

Yale University

Software frequently converts data from one representation to another and vice versa. Naively specifying both conversion directions separately is error prone and introduces conceptual duplication. Instead, bidirectional programming techniques allow programs to be written which can be interpreted in both directions. However, these techniques often employ programming idioms that are alien to non-experts, via restricted, specialised combinator libraries. Instead, we introduce a framework for composing bidirectional programs monadically, enabling bidirectional programming with familiar abstractions in functional languages such as Haskell. We demonstrate the generality of our approach applied to parsers/printers, lenses, and generators/predicates. We show how to leverage compositionality and equational reasoning for the verification of round-tripping properties for such monadic bidirectional programs.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_6

Li-yao Xia

University of Pennsylvania

Dominic Orchard

University of Kent, UK

United Kingdom

Meng Wang

University of Bristol, UK

United Kingdom

Site-graph rewriting languages, such as Kappa or BNGL, offer parsimonious ways to describe highly combinatorial systems of mechanistic interactions among proteins, which may be then simulated efficiently. Modelling mechanisms involving counting (a number of phosphorylated sites for instance) require an exponential number of rules in Kappa, and may not be simulated efficiently in BNGL.

In this paper, we extend Kappa to deal both parsimoniously and efficiently with counters. We propose a single push-out semantics for Kappa with counters, we show how to compile Kappa with counters into Kappa without counters (without requiring more rules, nor damaging the performance of the simulation), and we design a static analysis, based on affine relationships, to relate the value of each counter to their meaning and bound their values.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_7

Pierre Boutillier

Ioana Cristescu

INRIA, France

Jerome Feret

INRIA Paris

France

We consider a class of interrupt-driven programs that model the kernel API libraries of some popular real-time embedded operating systems and the synchronization mechanisms they use. We define a natural notion of data races and a happens-before ordering for such programs. The key insight is the notion of disjoint blocks to define the synchronizes-with relation. This notion also suggests an efficient and effective lockset based analysis for race detection. It also enables us to define efficient ‘‘sync-CFG’’ based static analyses for such programs, which exploit data-race freedom. We use this theory to carry out static analysis on the FreeRTOS kernel library to detect races and to infer simple relational invariants on key kernel variables and data-structures.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_25

Nikita Chopra

R Rekha

Deepak D'Souza

Popular programming techniques such as shallow embeddings of Domain Specific Languages (DSLs), finally tagless or object algebras are built on the principle of compositionality. However, existing programming languages only support simple compositional designs well, and have limited support for more sophisticated ones. This paper presents the F+i calculus, which supports highly modular and compositional designs that improve on existing techniques. These improvements are due to the combination of three features: disjoint intersection types with a merge operator; parametric (disjoint) polymorphism; and BCD-style distributive subtyping. The main technical challenge is F+i’s proof of coherence. A naive adaptation of ideas used in System F’s parametricity to canonicity (the logical relation used by F+i to prove coherence) results in an ill-founded logical relation. To solve the problem our canonicity relation employs a different technique based on immediate substitutions and a restriction to predicative instantiations. Besides coherence, we show several other important meta-theoretical results, such as type-safety, sound and complete algorithmic subtyping, and decidability of the type system. Remarkably, unlike F<:’s bounded polymorphism, disjoint polymorphism in F+i supports decidable type-checking.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_14

Xuan Bi

Standard Chartered Bank

China

Ningning Xie

The University of Hong Kong

China

Bruno C. d. S. Oliveira

The University of Hong Kong, Hong Kong

Hong Kong

Tom Schrijvers

KU Leuven

Normal-form bisimulation, also known as open bisimulation, is a coinductive technique for higher-order program equivalence in which programs are compared by looking at their essentially infinitary tree-like normal forms, i.e. at their Böhm or Levy-Longo trees. The technique has been shown to be useful not only when proving metatheorems about lambda-calculi and their semantics, but also when looking at concrete examples of terms. In this paper, we show that there is a way to generalise normal-form bisimulation to calculi with algebraic effects, à la Plotkin and Power. We show that some mild conditions on monads and relators, introduced by Dal Lago, Gavazzo, and Levy, are enough to prove that the obtained notions of bisimulation are congruences, thus sound for contextual equivalence. We exemplify the technique for various kinds of effects, including probabilistic choice, global store, and the ticking monad.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_10

Ugo Dal Lago

University of Bologna / Inria

Italy

Francesco Gavazzo

Best paper nomination

Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs.

We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the language.

We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_9

Dylan McDermott

University of Cambridge

Alan Mycroft

University of Cambridge

Incremental computation has recently been studied using the concepts of change structures and derivatives of programs, where the derivative of a function allows updating the output of the function based on a change to its input. We generalise change structures to change actions, and study their algebraic properties. We develop change actions for common structures in computer science, including directed-complete partial orders and Boolean algebras. We then show how to compute derivatives of fixpoints. This allows us to perform incremental evaluation and maintenance of recursively defined functions with particular application generalised Datalog programs. Moreover, unlike previous results, our techniques are modular in that they are easy to apply both to variants of Datalog and to other programming languages.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_19

Michael Peyton Jones

IOHK

United Kingdom

Mario Alvarez-Picallo

University of Oxford

Alexander Eyers-Taylor

Semmle

United Kingdom

C.-H. Luke Ong

University of Oxford

United Kingdom

Algebraic effects and handlers are a powerful abstraction mechanism to represent and implement control effects. In this work, we study their extension with parametric polymorphism that allows abstracting not only expressions but also effects and handlers. Although polymorphism makes it possible to reuse and reason about effect implementations more effectively, it has long been known that naive combination of polymorphic effects and let-polymorphism breaks type safety. While type safety can often be gained by restricting let-bound expressions—e.g., by adopting value restriction or weak polymorphism—we propose a complementary approach, which restricts, instead of let-bound expressions, handlers. Our key observation is, informally speaking, that a handler is safe if resumptions from the handler do not interfere with each other. To formalize our idea, we define a call-by-value lambda calculus that supports let-polymorphism and polymorphic algebraic effects and handlers, design a type system that rejects interfering handlers, and prove type safety of our calculus.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_13

Taro Sekiyama

National Institute of Informatics

Japan

Atsushi Igarashi

Kyoto University, Japan

Japan

Incremental computation requires propagating changes and reusing intermediate results of base computations. Derivatives, as produced by static differentiation, propagate changes but do not reuse intermediate results, leading to wasteful recomputation. As a solution, we introduce conversion to Cache-Transfer-Style, an additional program transformations producing purely incremental functional programs that create and maintain nested tuples of intermediate results. To prove CTS conversion correct, we extend the correctness proof of static differentiation from STLC to untyped $\lambda$-calculus via step-indexed logical relations, and prove sound the additional transformation via simulation theorems. To show ILC-based languages can improve performance relative to from-scratch recomputation, and that CTS conversion can extend its applicability, we perform an initial performance case study. We provide derivatives of primitives for operations on collections and incrementalize selected example programs using those primitives, confirming expected asymptotic speedups.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_20

Paolo G. Giarrusso

TU Delft, The Netherlands

Italy

Yann Régis-Gianas

IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2

France

Philipp Schuster

University of Tübingen, Germany

Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed $\pi$-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to a lock discipline of acquire-release. While this generalization greatly increases the range of programs that can be written, the gain in expressiveness comes at the cost of deadlock-freedom, a property which holds for many linear session type systems. In this paper, we develop a type system for logically-shared sessions in which types capture not only the interactive behavior of processes but also constrain the order of resources (i.e., shared processes) they may acquire. This type-level information is then used to rule out cyclic dependencies among acquires and synchronization points, resulting in a system that ensures deadlock-free communication for well-typed processes in the presence of shared sessions, higher-order channel passing and recursive processes. We illustrate our approach on a series of examples, showing that it rules out deadlocks in circular networks of both shared and linear recursive processes, while still being permissive enough to type concurrent implementations of shared imperative data structures as processes.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_22

Stephanie Balzer

Carnegie Mellon University

United States

Bernardo Toninho

Imperial College London

Frank Pfenning

Carnegie Mellon University, USA

We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing to use tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to generate verified code automatically. Meta-F* is implemented as an F* effect, which, given the powerful effect system of F*, heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F* type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F* provides substantial gains in proof development, efficiency, and robustness.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_2

Guido Martínez

CIFASIS-CONICET, Argentina

Argentina

Danel Ahman

University of Ljubljana

Slovenia

Victor Dumitrescu

Nomadic Labs Paris

France

Nick Giannarakis

Princeton University

Chris Hawblitzel

Microsoft Research

Cătălin Hriţcu

Inria Paris

France

Monal Narasimhamurthy

University of Colorado, Boulder

United States

Zoe Paraskevopoulou

Princeton University

United States

Clément Pit-Claudel

MIT CSAIL

Jonathan Protzenko

Microsoft Research, Redmond

United States

Tahina Ramananandro

Microsoft Research, n.n.

United States

Aseem Rastogi

Microsoft Research

India

Nikhil Swamy

Microsoft Research

United States

Modern software is no more developed in a single programming language. Instead, programmers tend to exploit cross-language interoperability mechanisms to combine code stemming from different languages, and thus yielding fully-fledged multi-language programs. Whilst this approach enables developers to benefit from the strengths of each single-language, on the other hand it complicates the semantics of such programs. Indeed, the resulting multi-language does not meet any of the semantics of the combined languages. In this paper, we broaden the boundary functions-based approach à la Matthews and Findler to propose an algebraic framework that provides a constructive mathematical notion of multi-language able to determine its semantics. The aim of this work is to overcome the lack of a formal method (resp., model) to design (resp., represent) a multi-language, regardless of the inherent nature of the underlying languages. We show that our construction ensures the uniqueness of the semantic function (i.e., the multi-language semantics induced by the combined languages) by proving the initiality of the term model (i.e., the abstract syntax of the multi-language) in its category.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_11

Samuele Buro

Università degli Studi di Verona

Isabella Mastroeni

University of Verona, Italy

Italy

Big-step and small-step are two popular flavors of operational semantics. Big-step is often seen as a more natural transcription of informal descriptions, as well as being more convenient for some applications such as interpreter generation or optimization verification. Small-step allows reasoning about non-terminating computations, concurrency and interactions. It is also generally preferred for reasoning about type systems. Instead of having to manually specify equivalent semantics in both styles for different applications, it would be useful to choose one and derive the other in a systematic or, preferably, automatic way.

Transformations of small-step semantics into big-step have been investigated in various forms by Danvy and others. However, it appears that a corresponding transformation from big-step to small-step semantics has not had the same attention. We present a fully automated transformation that maps big-step evaluators written in direct style to their small-step counterparts. Many of the steps in the transformation, which include CPS-conversion, defunctionalization, and various continuation manipulations, mirror those used by Danvy and his co-authors. For many standard languages, including those with either call-by-value or call-by-need and those with state, the transformation produces small-step semantics that are close in style to handwritten ones. We evaluate the applicability and correctness of the approach on 20 languages with a range of features.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_8

Kathleen Fisher

Tufts University

United States

Ferdinand Vesely

Swansea University

United Kingdom

We define a new denotational semantics for a first-order probabilistic programming language in terms of probabilistic event structures. This semantics is intensional, meaning that the interpretation of a program contains information about its behaviour throughout execution, rather than a simple distribution on return values. In particular, occurrences of sampling and conditioning are recorded as explicit events, partially ordered according to the data dependencies between the corresponding statements in the program.
This interpretation is adequate: we show that the usual measure-theoretic semantics of a program can be recovered from its event structure representation. Moreover it can be leveraged for MCMC inference: we prove correct a version of single-site Metropolis-Hastings with incremental recomputation, in which the proposal kernel takes into account the semantic information in order to avoid performing some of the redundant sampling.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_12

Simon Castellan

Imperial College London, UK

Hugo Paquet

University of Cambridge

Secure compilers generate compiled code that withstands many target-level attacks such as alteration of control flow, data leaks or memory corruption. Many existing secure compilers are proven to be fully abstract, meaning that they reflect and preserve observational equivalence. Fully abstract compilation is strong and useful but, in certain cases, comes at the cost of requiring expensive runtime constructs in compiled code. These constructs may have no relevance for security, but are needed to accommodate differences between the source and target languages that fully abstract compilation necessarily needs. As an alternative to fully abstract compilation, this paper explores a different criterion for secure compilation called robustly safe compilation or RSC. Briefly, this criterion means that the compiled code preserves relevant safety properties of the source program against all adversarial contexts interacting with the compiled program. We show that RSC can be proved more easily that fully abstract compilation and also often results in more efficient code. We also develop three illustrative robustly- safe compilers and, through them, develop two different proof techniques for establishing that a compiler attains RSC. Through these, we also establish that proving RSC is simpler than proving fully abstraction.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_17

Marco Patrignani

Stanford University & CISPA Helmholtz Center for Information Security

United States

Deepak Garg

Max Planck Institute for Software Systems

Germany

Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect. These techniques rely on the concept of a grace period: nodes that should be freed are placed on a deferred free list, and all threads obey a protocol to ensure that the deallocating thread can detect when all possible readers have completed their use of the object. This provides an approach to safe deallocation, but only when these subtle protocols are implemented correctly. We present a static type system to ensure correct use of RCU memory management: that nodes removed from a data structure are always scheduled for subsequent deallocation, and that nodes are scheduled for deallocation at most once. As part of our soundness proof, we give an abstract semantics for RCU memory management primitives which captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_4

Ismail Kuru

Drexel University

United States

Colin Gordon

Drexel University

United States

Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions—so called ``sequence point violations''. These aspects should be accounted for in verification because C compilers exploit them. We present a verification condition generator (vcgen) that enables one to semi-automatically prove the absence of undefined behavior in a given C program for any evaluation order. The key novelty in our approach is a symbolic execution algorithm that computes a frame at the same time as a postcondition. The frame is used to automatically determine how resources should be distributed among subexpressions. We prove correctness of our vcgen with respect to a new monadic definitional semantics of a subset of C. This semantics is modular and gives a concise account of non-determinism in C. We have implemented our vcgen as a tactic in the Coq interactive theorem prover, and have proved correctness of it using a separation logic for a new monadic definitional semantics of a subset of C.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_3

Dan Frumin

Radboud University

Léon Gondelman

LRI, Université Paris-Sud

Robbert Krebbers

Delft University of Technology

Netherlands

We present a machine-checked extension of the program logic Iris with time credits and time receipts, two dual means of reasoning about time. Whereas time credits are used to establish an upper bound on a program’s execution time, time receipts can be used to establish a lower bound. More strikingly, time receipts can be used to prove that certain undesirable events—such as integer overflows—cannot occur until a very long time has elapsed. We present several machine-checked applications of time credits and time receipts, including an application where both concepts are exploited.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_1

Glen Mével

Jacques-Henri Jourdan

CNRS, LRI, Université Paris-Sud

France

François Pottier

Inria, France

France

A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_15

Beniamino Accattoli

Inria & Ecole Polytechnique

Giulio Guerrieri

University of Bath

United Kingdom

Maico Leberle

Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, at the exception of the definition of conversion, which is based on a specific notion of reduction $\rightarrow_{\beta *}$, corresponding to $\beta$-reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction $\rightarrow_{\beta \sigma}$ allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of $\rightarrow_{\beta \sigma}$ and strong normalization of both $\rightarrow_{\beta \sigma}$ and $\rightarrow_{\beta *}$. Using these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction $\rightarrow_{\beta \sigma}$ is used to define a cut elimination procedure adapted to predicate subtyping. Its use to study the properties of predicate subtyping is illustrated with a proof of consistency.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-030-17184-1_16

Frédéric Gilbert