Write a Blog >>
Tue 20 Jun 2017 14:00 - 14:20 at Vertex WS217 - C Chair(s): Martin Berger

In this paper we consider the problem of certified static checking of module-like constructs of programming languages. We argue that there are algorithms and properties related to modules that can be defined and proven in abstract way. We advocate the design of a generic Coq library, which is aimed to provide three building blocks for each checking mechanism: propositional, computable, and correctness proofs. Implemented part of the library is justified by applying it to a certified static checker of an extension of STLC.

Tue 20 Jun

FTfJP-2017-papers
14:00 - 15:30: FTfJP 2017 - C at Vertex WS217
Chair(s): Martin Berger
FTfJP-2017-papers14:00 - 14:20
Talk
Julia BelyakovaSouthern Federal University
Pre-print
FTfJP-2017-papers14:20 - 14:55
Talk
Paola GianniniUniversita' del Piemonte Orientale, Marco ServettoVictoria University of Wellington, Elena ZuccaUniversity of Genova
FTfJP-2017-papers14:55 - 15:30
Talk
Marianna RapoportUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Canada