Kathrin Stark
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 6 in the filters
on a stage with
- Alberto Momiglianoonce
- Aliya Hameeronce
- Andreas Abelonce
all 16 in the filters
who talks about the same things
- Théo Winterhalter14 talks
- Andrew W. Appel4 talks
- Matthieu Sozeau14 talks
- Ohad Kammar19 talks
- Michel Steuwer17 talks
- Steve Zdancewic19 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… | ||
| A Verified Foreign Function Interface Between Coq and C | POPL 2025 | 2025-01-19 |
VeriFFI provides a verified foreign-function interface that translates Coq dependent types and Coq functional models into VST specs so C functions, once proved… | ||
| Towards a Certified Proof Checker for Deep Neural Network Verification | LOPSTR 2023 | 2023-10-23 |
A formally verified proof checker for deep neural network verification is implemented in Imandra and extracts to native OCaml, using Simplex proof certificates… | ||
| POPLMark reloaded: Mechanizing proofs by logical relations | ICFP 2020 | 2020-08-23 |
Proposes a benchmark that mechanizes logical-relation proofs by proving strong normalization via Kripke-style logical relations for simply-typed lambda… | ||
| Autosubst 2: Reasoning with de Bruijn Terms and Substitutions | CoqPL 2020 | 2020-01-25 |
Presenter: Kathrin Stark
Presented at CoqPL'20, part of POPL 2020. | ||
| Coq a la Carte: A Practical Approach to Modular Syntax With Binders | CPP 2020 | 2020-01-20 |
Presents a Coq workflow that achieves practical modular syntax by using direct injections of variant copies instead of functor fixed points, plus generated… | ||
| nothing matches | ||