Alejandro Díaz-Caro

Departamento de Ciencia y Tecnología, Universidad Nacional de Quilmes
Instituto de Ciencias de la Computación (CONICET/Universidad de Buenos Aires)

An overview on the quantum control approach to the lambda calculus

Abstract: In this talk I will start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. I will give an overview of the line of research of the quantum control within the lambda calculus, ranging from untyped calculi up to categorical and realizability models. I will try to summarize the last ~20 years of research in this area, from van Tonder and Arrighi-Dowek's seminal works until today.

Alexandra Silva

Department of Computer Science, University College London

Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

Abstract: Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this talk, we will explore the (co)algebraic properties of GKAT. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then use coequations to provide a precise characterization of the behaviors of GKAT expressions and prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics. If time permits, we will also discuss how coequations can play a role in completeness proofs more generally. This is joint work with Todd Schmid, Tobias Kappé, and Dexter Kozen.

Giulio Guerrieri

Department of Computer Science, University of Bath

Understanding the lambda-calculus via (non-)linearity and rewriting.

Abstract: The lambda-calculus is the model of computation underlying functional programming languages and proof assistants. Actually, there are many lambda-calculi, depending on the evaluation mechanism (e.g., call-by-name, call-by-value, call-by-need) and computational features that the calculus aims to model (e.g., plain functional, non-deterministic, probabilistic, infinitary).

The existence of different paradigms is troubling because one apparently needs to study the theory and semantics of each one separately.

We propose a unifying and uniform meta-theory of lambda-calculi, where the study is rooted on a unique core language, the bang calculus, a variant of the lambda-calculus inspired by Girard's linear logic and Levy's Call-by-Push-Value: a bang operator marks which resources can be duplicated or discarded.

The bang calculus subsumes both call-by-name and call-by-value. A property studied in the bang calculus is automatically translated in the corresponding property for the call-by-name lambda-calculus and the call-by-value lambda-calculus, thanks to two different embeddings of the lambda-calculus in the bang calculus. These embeddings are grounded on proof theory: they are an adaptation of Girard's two translations of intuitionistic logic into linear logic.

Advanced computational features are usually obtained by adding new operators to a core language. Instead of studying the operational properties of the extended language from scratch, we propose a simple method to study them modularly: if an operational property holds in the core language and in the new operators separately, then a simple test of good interaction between core language and new operators guarantees that the property lifts to the whole extended language. This approach is first developed in abstract rewriting systems.