SYSTEMF @ EPFL
/ˈsɪstəmˌɛf/
We're a programming languages, formal methods, and systems engineering lab at EPFL, led by Clément Pit-Claudel. We use (and invent!) mathematical formalisms and interactive tools to explore new ways to develop computer systems.
Our main goal is to build small, fast, and completely verified components for critical systems, at reasonable cost. We call this full assurance, without compromise. We think we can get there with a combination of machine-checked proofs of correctness, hardware-software co-design, low-level compiler engineering, and new tools and approaches for interactive theorem proving.
Beyond research, we think about teaching a lot, and more generally about how to democratize programming and verification. At EPFL, we're responsible for teaching Software Construction (undergraduate level, ~400 students) and Interactive Theorem Proving (graduate level).
We're excited to explore new collaborations, and the lab accepts students and interns at all levels. If you're interested in compilers, systems engineering, UIs for programming and interactive theorem proving, or logics for verification and proof systems, get in touch!
Finally: we're new! The lab was created in January 2023, so a lot of relevant information is still on Prof. Pit-Claudel's personal webpage, including a complete list of previous publications and old statements on research and teaching.