Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revisionBoth sides next revision
research:csec [2018/03/21 10:12] – etanterresearch:csec [2018/03/21 10:13] – etanter
Line 8: Line 8:
  
 === March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) === === March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) ===
- 
-==== Preliminary Program ==== 
- 
-{{ :research:csec:kickoff-program.png?nolink&800 |}} 
  
 ==== Titles & abstracts of the talks (most slides are now available as well!) ==== ==== Titles & abstracts of the talks (most slides are now available as well!) ====
Line 46: Line 42:
     * ++ 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 |}}