Logic and Foundations of Programming Languages Day
May 21, 2018
Departamento de Computación, FCEN, Universidad de Buenos Aires
Pabellón 1, Ciudad Universitaria, Buenos Aires
The LoReL team and the Laboratoire International Associé INFINIS organize a day on logic and foundations of programming languages. The intention is to bring together researchers from the Río de la Plata region. We will profit from the visit of several French colleagues who will be in the region on that date.
09:30 – 10:00 Welcome coffee
10:00 – 10:25 Beta Ziliani: Introducing Mtac2: first-class tactics with first-class types in Coq
10:25 – 10:50 Benoît Valiron: From symmetric pattern-matching to quantum control
10:50 – 11:15 Alejandro Díaz-Caro: A lambda calculus for density matrices
11:15 – 11:40 Mate Break
12:55 – 14:40 Lunch
14:40 – 15:05 Alexandre Miquel: Implicative algebras: a new foundation for realizability and forcing
15:05 – 15:30 Mauricio Guillermo: TBA
15:30 – 15:55 Pierre Pradic: TBA
15:55 – 16:20 Luc Pellissier: TBA
16:20 – 16:45 Mate Break
Andrés Viso (email@example.com)
Alejandro Díaz-Caro (firstname.lastname@example.org)
- Beta Ziliani: Introducing Mtac2: first-class tactics with first-class types in Coq
Mtac2 is a novel language for building tactics in the Coq theorem prover. A tactic is a program which solves the current goal, perhaps creating new subgoals. The novelty in Mtac2 is that its tactics are written in the same language of the prover and, more importantly, have their types embedded in the language. Therefore, an Mtac2 tactic could precisely state in its type what kind of goals it is able to solve, leading to self-documented, more-maintainable tactics.
In this talk I will introduce the main ideas behind Mtac2, and its application in the widely-used Iris logic framework.
- Benoît Valiron: From symmetric pattern-matching to quantum control
From a programmer’s perspective, quantum algorithms are simply classical algorithms having access a special kind of memory featuring particular operations: quantum operations. They therefore feature two kinds of control flow. One is purely conventional and is concerned in the classical part of the algorithm. The other — dubbed quantum control — is more elusive and still subject to debate: if the notion of quantum test is reasonnably consensual, the quantum counterpart of loops is still not believed to be meaningful.
In this talk, we argue that, under the right circumstances, a reasonnable notion of quantum loop is possible. To this aim, we propose a typed, reversible language with lists and fixpoints, extensible to linear combinations of terms. The language admits a reduction strategy in the spirit of algebraic lambda-calculi. Under the restriction of structurally recursive fixpoints, it is shown to capture unitary operations. It is expressive enough to represent several of the unitaries one might be interested in expressing.
- Alejandro Díaz-Caro: A lambda calculus for density matrices
In this talk I will present two flavors of a quantum extension to the lambda calculus. The first one, λρ, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, λρ°, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach. In addition, I will comment on some advances on ongoing works with Malena Ivnisky and Henrán Melgratti (fix point operator), Agustín Borgna (translation to a well-known quantum lambda calculus, and possible extension of the languages), Lucas Romero (polymorphisme) and Alan Rodas and Pablo E. Martínez López (a Haskell implementation).
- Antonio Bucciarelli: n-dimensional Boolean algebras
n-dimensional Boolean algebras (nBA) generalise BA to the case of n perfectly symmetric truth values. The talk provides an overview of their algebraic structure and of the corresponding propositional calculus (joint work in progress with A.Ledda, F. Paoli and A. Salibra)
- Olivier Carton: Randomness with constraints
We first recall the definition of normality which is a kind of weak randomness. We show how some constraints can be imposed without loosing randomness. We even give an sharp upper bound of what can be imposed.
- Santiago Figueira: TBA
- Alexandre Miquel: Implicative algebras: a new foundation for realizability and forcing
- Mauricio Guillermo: TBA
- Pierre Pradic: TBA
- Luc Pellissier: TBA
- Delia Kesner: Call by need, neededness and all that
We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection type system called V. Interestingly, system V also allows to syntactically identify all the weak-head needed redexes of a term.
- Andrés Viso: TBA
- Pablo Barenbaum: TBA