Type-Preserving Compilation of Class-Based Languages

What is a program?

• A series of instructions that a computer can execute to produce some output given some input.

• These instructions are written in a programming language.

Programs are like recipe

There’s a lot of programming languages!

An intriguing announcement

Subject: Dotty open-sourced
From: martin odersky <martin.odersky@epfl.ch>
To: <scala-internals@googlegroups.com>
Date: Feb 18 2014 19:06:07 +0200

A couple of days ago we open sourced Dotty, a research
platform for new language concepts and
compiler technologies for Scala.
[...]
Right now, there's a (very early) compiler frontend for
a subset of Scala. We'll work on fleshing this out [...]

So what is a compiler?

Compiling is like Translating

Collaborative development

Doing a PhD

Doing a PhD

Doing a PhD

Doing a PhD

My PhD

• Worked on many things to make Scala 3.0 a reality.
• One area of focus: the type checker.

The type checker is like a Chef 🧑‍🍳

2021: Scala 3.0 is out!

… but now I have to write a thesis 🤔

• How can I formalize the work we did?

A source of inspiration

My own paper!

The plan

• Extend Pathless Scala to support more language features.
• Prove Type Safety.

Type Safety

If a language is type safe then programs which are accepted by the type checker can be executed without getting stuck.

… But proving type safety is hard!

An alternative approach:
Type-Preserving Compilation

• If Language B is type-safe, then Language A will also be type-safe.
• In our case, Language A will be Pathless Scala.
• But what to pick as Language B?

Standing on the shoulders of giants

The DOT family tree 👪

The plan

The plan

The plan

When the recipe can’t be translated

Extending the DOT type safety proof

• Unlike FJ, the DOT proof is mechanized: it’s a program we can improve!

Back to the plan

A hint

From: Sandro Stucki
Date: Thu, 12 May 2022 18:33:52 +0200

Hi Guillaume!

Aah, you're deep in the DOT swamp now, I see ;-)

[...]

I just remembered that Tiark and Nada use a non-standard
type safety proof in that paper [...]

Let’s change the type safety theorem!

The final result

Thank you!

Questions?