Stream: Miscellaneous

Topic: Thesis defense for Clément Pit-Claudel

Clément Pit-Claudel (Nov 30 2021 at 07:32):

Hi all!

I'm defending my thesis on Thursday at 10AM Eastern Time (4PM Paris time). The topic is relational compilation and how to use it to generate low-level code that is both fast and trustworthy, in Coq (more details at https://www.csail.mit.edu/event/thesis-defense-relational-compilation-end-end-verification ).

The talk is public and will be livestreamed at https://mit.zoom.us/j/96451987305 ; feel free to join!

(And if you're curious about the topic but not a fan of Zoom calls, I wrote an intro about relational compilation at https://people.csail.mit.edu/cpitcla/thesis/relational-compilation.html .)

Clément Pit-Claudel (Dec 02 2021 at 19:37):

I passed! Thanks so much to everyone who attended the defense :)

Emilio Jesús Gallego Arias (Dec 02 2021 at 21:35):

Congrats! Unfortunately I couldn't attend due to scheduling conflicts, will there be a video recording released?

Julin S (Dec 03 2021 at 05:34):

Thanks for posting the meeting link here.

Karl Palmskog (Dec 06 2021 at 10:39):

hmm, how does the relational compilation stuff for Coq compare to CakeML's proof-producing synthesis ("frontend 1" here)? Is it mainly that the latter is more low-level, uses less automation, etc.?

Clément Pit-Claudel (Dec 08 2021 at 07:44):

Emilio Jesús Gallego Arias said:

Congrats! Unfortunately I couldn't attend due to scheduling conflicts, will there be a video recording released?

Yes, I will upload the video when I get time :)

Clément Pit-Claudel (Dec 08 2021 at 07:50):

Karl Palmskog said:

hmm, how does the relational compilation stuff for Coq compare to CakeML's proof-producing synthesis ("frontend 1" here)? Is it mainly that the latter is more low-level, uses less automation, etc.?

The CakeML stuff is awesome. We're using very similar techniques; the big difference is the kind of languages we're targeting. CakeML's translator bridges a much narrower gap (its target language is much closer to its source language), so the performance engineering and extensibility aspects are a lot less important (you don't need user extensions if you're always going to translate the same patterns in the same ways). This shows in the way state is handled: in most versions of their tool the CakeML folks use monadic sources when they want mutation in the target, whereas in Rupicola in most cases you use a more "intensional" encoding where non-monadic operations get translated to stateful ones (think translating replace_nth to a store at the corresponding offset in an array).

Clément Pit-Claudel (Dec 08 2021 at 07:51):

So I guess the summary is: CakeML's translator is a relational compiler like Rupicola. It solves the issue of going from a shallow to a deep embedding, like Rupicola, but not the issue of allowing user extensions to the compiler to generate fast low-level code directly from functional sources.

Karl Palmskog (Dec 08 2021 at 08:48):

thanks, then I guess I've been a relational compilation user for a while without knowing it. There is a lot of fiddling with the shallow side to make it work out as expected though.

Last updated: Sep 15 2024 at 13:02 UTC