Formal verification of Scala programs with Stainless
— Video
— Slides
@ Typelevel Summit Lausanne, June 2019
Hi, my name is Romain Ruetschi, or just Romac.
I help people write better software that is correct and does not crash at the Laboratory for Automated Reasoning and Analysis at EPFL in Lausanne, Switzerland.
My main areas of interest are related to functional programming, type theory, compiler construction, and formal verification of software. I like exploring these topics in Haskell, Scala, and Rust.
You can reach me on Twitter, Wire (@romac), Signal (@romac), or via Keybase.
PGP Key fingerprint (romain.ruetschi@gmail.com):
02A8 0B86 4B97 1E10 BDE3 EA5E 5122 3DE6 C814 84B9
— Video
— Slides
@ Typelevel Summit Lausanne, June 2019
— Slides
@ Formal Methods & Verified Software Meetup, EPFL, May 2018
— Slides
@ Tokyo University, August 2015
— Slides
+ Dimiter Petrov
@ EPFL, Lausanne, November 2014
I mainly work on Stainless, a verification framework for higher-order functional Scala programs developed at the LARA at EPFL.
Simple functional programming language with refinement types, powered by Inox. Crafted for my Refine your types! (see above).
Rust implementation of threshold Shamir's secret sharing.
Rust implementation of Merkle trees.
mdash is a Chrome extension which replaces the New Tab page with a light dashboard linked with your bookmarks.
Hackers at EPFL was an association which aimed to promote the hacking culture at EPFL.