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.91MiB

Fri 18 Jan

POPL-2019-Research-Papers
09:00 - 10:05: Research Papers - SRC Announcement & Keynote II at Sala I + II
Chair(s): Stephanie WeirichUniversity of Pennsylvania, USA
POPL-2019-Student-Research-Competition09:00 - 09:05
Awards
Niki VazouIMDEA Software Institute
Media Attached
POPL-2019-Research-Papers09:05 - 10:05
Talk
Brigitte PientkaMcGill University
Media Attached File Attached