GPCE 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Sun 17 Oct 2021 08:25 - 08:40 at Zurich C - GPCE/SLE Session 4 Chair(s): Mikhail Barash
Sun 17 Oct 2021 16:25 - 16:40 at Zurich C - GPCE/SLE Session 4 Chair(s): Eric Van Wyk

Most existing programming languages provide little support to formally state and prove properties about programs. Ad-ding such capabilities is far from trivial, as it requires significant re-engineering of the existing compilers and tools. This paper proposes a novel technique to write correct-by-con-struc-tion programs in languages without built-in verification capabilities, while maintaining the ability to use existing tools. This is achieved in three steps. Firstly, we give a shallow embedding of the language (or a subset) into a dependently typed language. Secondly, we write a program in that embedding, and we use dependent types to guarantee correctness properties of interest. Thirdly, we extract a program written in the original language, so that it can be used by the existing compilers and tools.

Our main insight is that it is possible to express all three steps in a single language that supports both dependent typ-es and reflection. Essentially, this allows us to express a program, its formal properties, and a compiler for it hand-in-hand, offering a lot of flexibility to programmers. We demonstrate this three-step approach by embedding a subset of the PostScript language in Agda, and illustrating it with several short examples. Thus we use the power of reflection to bring the benefits of dependent types to languages that had to go without them so far.

Sun 17 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
GPCE/SLE Session 4GPCE / SLE at Zurich C
Chair(s): Mikhail Barash University of Bergen
07:40
15m
Talk
A Concurrency Model for JavaScript with Cooperative CancellationVirtual
SLE
Tian Zhao University of Wisconsin-Milwaukee, Yonglun Li University of Wisconsin -- Milwaukee
07:55
15m
Talk
There Is More Than One Way to Zen Your PythonVirtual
SLE
Aamir Farooq Universiteit Twente, Vadim Zaytsev University of Twente, Netherlands
08:10
15m
Talk
Getting Grammars into Shape for Block-based EditorsVirtual
SLE
Mauricio Verano Merino Eindhoven University of Technology, Tom Beckmann Hasso Plattner Institute, Tijs van der Storm CWI; University of Groningen, Robert Hirschfeld Hasso Plattner Institute (HPI), University of Potsdam, Germany, Jurgen Vinju CWI; Eindhoven University of Technology
Pre-print
08:25
15m
Talk
Extracting The Power of Dependent TypesVirtual
GPCE
Artjoms Šinkarovs Heriot-Watt University, UK, Jesper Cockx TU Delft
08:40
20m
Live Q&A
Discussion, Questions, Answers
GPCE

15:40 - 17:00
GPCE/SLE Session 4SLE / GPCE at Zurich C -8h
Chair(s): Eric Van Wyk University of Minnesota, USA
15:40
15m
Talk
A Concurrency Model for JavaScript with Cooperative CancellationVirtual
SLE
Tian Zhao University of Wisconsin-Milwaukee, Yonglun Li University of Wisconsin -- Milwaukee
15:55
15m
Talk
There Is More Than One Way to Zen Your PythonVirtual
SLE
Aamir Farooq Universiteit Twente, Vadim Zaytsev University of Twente, Netherlands
16:10
15m
Talk
Getting Grammars into Shape for Block-based EditorsVirtual
SLE
Mauricio Verano Merino Eindhoven University of Technology, Tom Beckmann Hasso Plattner Institute, Tijs van der Storm CWI; University of Groningen, Robert Hirschfeld Hasso Plattner Institute (HPI), University of Potsdam, Germany, Jurgen Vinju CWI; Eindhoven University of Technology
Pre-print
16:25
15m
Talk
Extracting The Power of Dependent TypesVirtual
GPCE
Artjoms Šinkarovs Heriot-Watt University, UK, Jesper Cockx TU Delft
16:40
20m
Live Q&A
Discussion, Questions, Answers
GPCE