Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
research:csec [2018/03/21 10:12] – etanterresearch:csec [2019/07/02 20:56] (current) – etanter
Line 1: Line 1:
-====== CSEC: Certified Software Engineering in Coq / Kick-off Workshop ====== +====== CSEC: Certified Software Engineering in Coq ====== 
  
 The development of tools to construct software systems that respect a given specification is a major challenge of current and future research in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their effectiveness to prove correctness of important pieces of software like the C compiler of the CompCert project. Certified programming with dependent types is attracting a lot of attention recently, and Coq is the de facto standard for such endeavors, with an increasing amount of users, pedagogical material, and large-scale projects. Nevertheless, significant work remains to be done to make Coq more usable from a software engineering point of view. The development of tools to construct software systems that respect a given specification is a major challenge of current and future research in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their effectiveness to prove correctness of important pieces of software like the C compiler of the CompCert project. Certified programming with dependent types is attracting a lot of attention recently, and Coq is the de facto standard for such endeavors, with an increasing amount of users, pedagogical material, and large-scale projects. Nevertheless, significant work remains to be done to make Coq more usable from a software engineering point of view.
Line 7: Line 7:
  
  
-=== March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) ===+====== Kick-off Workshop: March 6-9, 2018 @ DCC ======
  
-==== 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**:
Line 46: Line 47:
     * ++ 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 |}}