Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| research:csec [2018/03/21 13:14] – etanter | research:csec [2019/07/02 23: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, | 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, | ||
| Line 7: | Line 7: | ||
| - | === March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) | + | ====== Kick-off Workshop: |
| ==== Titles & abstracts of the talks ==== | ==== Titles & abstracts of the talks ==== | ||