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:13] 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 ====== 
 + 
 +==== Titles & abstracts of the talks ==== 
 + 
 +<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**: