## Programming

#### Day, hour and place

Monday at 10am, IRIF

The calendar of events (iCal format).

In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.

#### Contact(s)

### Next talks

Programming

Monday November 4, 2024, 10AM, 3071

**Thierry Martinez** (INRIA) *Coq Deep Pattern-Matching using Small Inversion*

Most of the design challenges for this algorithm come from handling the equalities that appear at each level of deconstruction of dependent inductive values. I will compare three approaches: one proposed by Healfdene Goguen, Conor McBride, and James McKinna, which relies on the equivalence axiom between homogeneous and heterogeneous equalities (equivalent to the Uniqueness of Identity Proofs); a refinement proposed by Jesper Cockx, which avoids the need for axioms; and the encoding by small inversion, which moves the proofs of deconstruction of the dependencies from the term level to the type level. While these algorithms give an encoding of dependent pattern-matching into the Coq kernel, this discussion leads us to think about what could be a better primitive form of pattern-matching.

Programming

Monday November 18, 2024, 10AM, 3071

**Guillaume Baudart** (IRIF) *Natural Language Intermediate Representation for Mechanized Theorem Proving*

### Previous talks

#### Year 2024

Programming

Monday October 14, 2024, 10AM, 4071

**Pierre-Evariste Dagand** (IRIF) *A type-theoretic model of smart contracts*

Caught once again by my incurable curiosity, I have set out to delineate precisely what set smart contracts aside in the realm of programming languages.

This talk reports on some early results, modeling the semantics of smart contracts in a type-theoretic and monadic framework. The objective of this work is to support formal reasoning at the protocol level (that is, starting from a specification free from programming error).

We shall strive to stay on track and in good taste: the presentation will not cover any financial aspect of smart contracts.

Programming

Monday September 30, 2024, 10AM, 3071

**Gabriel Scherer** (IRIF) *Pattern-matching on mutable values: danger!*

We recall the overall compilation strategy of the OCaml compiler, and explain how to weaken its optimization information to remain correct on mutable data.

## Extended abstract

https://www.irif.fr/~scherer/research/mutable-patterns/mutable-patterns-mlworkshop2024-abstract.pdf