Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision |
research:csec [2018/03/21 10:12] – etanter | research:csec [2018/03/21 10:14] – etanter |
---|
=== March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) === | === March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) === |
| |
==== Preliminary Program ==== | ==== Titles & abstracts of the talks ==== |
| |
{{ :research:csec:kickoff-program.png?nolink&800 |}} | <note new> |
| Slides of the talks are now available! Expand the abstracts to see the link. |
| </note> |
| |
==== Titles & abstracts of the talks (most slides are now available as well!) ==== | |
| |
**Guillaume Munch-Maccagnoni**: | **Guillaume Munch-Maccagnoni**: |
* ++ Towards typed-tactics in Coq: the what, the why, and the how | The term "tactics" is heavily overloaded, sometimes meaning small-and-simple primitives of the base theory of the prover, sometimes meaning very sophisticated meta-programs. One way or another, most tactic languages provide very loose types for tactics, making them hard to compose and maintain. In this talk I will first provide some basic understanding of tactics and tactic languages, and then present the latest achievements in a new and yet fairly unexplored view of tactics: tactics typed in the base logic of the prover. In particular, I will talk about the language Mtac2, and its application in the widely-used Iris logic framework. {{research:csec:ziliani-mtac2.pdf|slides}}++ | * ++ Towards typed-tactics in Coq: the what, the why, and the how | The term "tactics" is heavily overloaded, sometimes meaning small-and-simple primitives of the base theory of the prover, sometimes meaning very sophisticated meta-programs. One way or another, most tactic languages provide very loose types for tactics, making them hard to compose and maintain. In this talk I will first provide some basic understanding of tactics and tactic languages, and then present the latest achievements in a new and yet fairly unexplored view of tactics: tactics typed in the base logic of the prover. In particular, I will talk about the language Mtac2, and its application in the widely-used Iris logic framework. {{research:csec:ziliani-mtac2.pdf|slides}}++ |
| |
| |
| ==== Program ==== |
| |
| {{ :research:csec:kickoff-program.png?nolink&800 |}} |
| |
| |