En poursuivant votre navigation sur ce site, vous acceptez l'utilisation d'un simple cookie d'identification. Aucune autre exploitation n'est faite de ce cookie. OK

Audiovisual Mathematics Library

Audiovisual Mathematics Library

Documents Kerjean, Marie 3 results

Filter
Select: All / None
Q
K | F x r
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

An introduction to Differential Linear Logic - Kerjean, Marie (Author of the conference) | CIRM H

Multi angle

In this talk, we introduce the syntax and semantics of Differential Linear Logic. We explain how its rules relate to Linear Logic's rules, and give informal intuitions in terms of functions and distributions. We show how its cut-elimination rules are a reflection of basic calculus rules. We also review Differential Lambda-calculus, with matching intuitions. At the end of the talk, we briefly review two recent development about Differential Linear Logic, in terms of Laplace transformation and co-promotion.[-]
In this talk, we introduce the syntax and semantics of Differential Linear Logic. We explain how its rules relate to Linear Logic's rules, and give informal intuitions in terms of functions and distributions. We show how its cut-elimination rules are a reflection of basic calculus rules. We also review Differential Lambda-calculus, with matching intuitions. At the end of the talk, we briefly review two recent development about Differential ...[+]

03B47 ; 03B70 ; 18C50 ; 68Q55

Bookmarks

Cochez un panier pour y ajouter l'enregistrement. Décochez-le pour l'en enlever.

4

Manage my selections

Report an error
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Differential linear logic extended to differential operators - Kerjean, Marie (Author of the conference) | CIRM H

Multi angle

Differential Linear Logic adds to the linear logic the possibility to linearize non-linear proofs. We show how that accounts for the resolution of a differential equation, and extend differential linear logic to linear partial differential equations with constant coefficients. We explain how this result stems from the interpretation of linear logic formulas as reflexive vector spaces.

03B70 ; 68Q55 ; 46A04

Bookmarks

Cochez un panier pour y ajouter l'enregistrement. Décochez-le pour l'en enlever.

4

Manage my selections

Report an error
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Coq/Rocq tutorial: Ssreflect tactics and the MathComp library - Kerjean, Marie (Author of the conference) | CIRM H

Multi angle

In this talk, we introduce the Ssreflect tactic language, as used in the Mathematical Components library. We will focus on the tactics used to make formalization work lighter and easier to maintain.

03B35

Bookmarks

Cochez un panier pour y ajouter l'enregistrement. Décochez-le pour l'en enlever.

4

Manage my selections

Report an error

List: nb of elts/page

Select: All / None