Théo Winterhalter
where else to find them
bluesky:theowinterhalter.bsky.social
what they talk about
all 4 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 22 in the filters
who talks about the same things
- Nicolas Tabareau14 talks
- Cătălin Hriţcu16 talks
- Cezar-Constantin Andrici8 talks
- Guido Martínez10 talks
- Matthieu Sozeau14 talks
- Danel Ahman7 talks
| title | conference | date |
|---|---|---|
| Sulfur: Substitution Generation using a Logical Framework | RocqPL 2026 | 2026-01-17 |
A Coq/Rocq plugin reimplements Autosubst’s costly asimpl by reflective tactic reification: it generates concrete de Bruijn-based syntax, translates terms into… | ||
| Bounded Sort Polymorphism with Elimination Constraints | POPL 2026 | 2026-01-11 |
Extends sort polymorphism with elimination constraints that record which sorts may eliminate into which, implements the system in the Rocq prover, and proves… | ||
| Towards formally secure compilation of verified F* programs against unverified ML(…) | PriSC 2026 | 2026-01-11 |
Framework written and verified in F compiles terminating higher-order IO F programs to a deeply embedded ML-like language with an end-to-end mechanized proof… | ||
| Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally | POPL 2026 | 2026-01-11 |
Claims a type theory LRTT that adds local rewrite rules via prenex abstraction over computation rules and a prototype implemented as a Rocq extension with all… | ||
| SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* | ICFP 2025 | 2025-10-12 |
SecRef is a secure-compilation framework for F that enforces verified programs’ assumptions about dynamically shared ML-style mutable references by inserting… | ||
| The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography | CPP 2024 | 2024-01-15 |
Coq is used to connect Hacspec, Jasmin and SSProve into an automated pipeline that produces: a functional Hacspec spec, an imperative SSProve spec, and… | ||
| Securing Verified IO Programs Against Unverified Code in F* | POPL 2024 | 2024-01-14 |
A verified secure compilation pipeline for F programs that perform IO, called SCIO, compiles verified code to a smaller F target and enforces assumptions at… | ||
| Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ... | PriSC 2023 | 2023-01-21 |
Secure compilation chain for an F subset with IO converts static specs into runtime checks and adds a linking-time reference monitor that blocks forbidden… | ||
| Verifying non-terminating programs with IO in F* | HOPE 2022 | 2022-09-11 |
Defines an F effect that specifies IO for both terminating and potentially non-terminating programs, implements an example echo server and most of a simple web… | ||
| The Taming of the Rew: A Type Theory with Computational Assumptions | POPL 2021 | 2021-01-17 |
Rewriting Type Theory lets users add user-defined rewrite rules as computational assumptions that the type checker applies automatically, not as… | ||
| The Taming of the Rew: A Type Theory with Computational Assumptions | POPL 2021 | 2021-01-17 |
Adds Rewriting Type Theory to dependently typed systems so user-supplied rewrite rules run automatically during typechecking instead of requiring explicit… | ||
| nothing matches | ||