Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 09:05 - 10:05 at Sala I + II - SRC Announcement & Keynote II Chair(s): Stephanie Weirich

Mechanizing formal systems and proofs about them plays an important role in establishing trust in programming languages and verifying software systems in general. Over the past decades, we have seen significant progress and success: the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheory of programming languages; the development of the first verified compiler in Coq demonstrated the feasibility and value of building verified compilers. Today, mechanizing proofs is a stable fixture in the daily life of programming languages researchers.

One might be tempted to assume that all is well – yet, the reality is that we seem to accept the status quo and focus on engineering solutions to get the next job done, although mechanizations can be time consuming and require substantial (sometimes heroic) effort. In this talk I will argue that we should strive to develop high-level abstractions, primitives, and tools to standardize common tasks and operations arising when working with formal systems and proofs about them.

Taking a look back at some of the foundational theoretical ideas and choices that underly type-theoretic proof environments today, I will survey recent achievements and sketch a dependently typed language that would make it easier to represent, maintain, and communicate formal systems and proofs about them – an elegant proof language for a more civilized age.

Slides (mech_meta_popl19.pdf)2.92MiB

Fri 18 Jan

Displayed time zone: Belfast change

09:00 - 10:05
SRC Announcement & Keynote IIStudent Research Competition / Research Papers at Sala I + II
Chair(s): Stephanie Weirich University of Pennsylvania, USA
SRC Announcement
Student Research Competition
Niki Vazou IMDEA Software Institute
Media Attached
Mechanized Metatheory - The Next Chapter
Research Papers
Brigitte Pientka McGill University
Media Attached File Attached