Grigore Rosu
where else to find them
what they talk about
where they keep going back
no series more than once — all 5 in the filters
on a stage with
- Xiaohong Chen2×
- Kartik Talwaronce
- Lucas Peñaonce
all 5 in the filters
who talks about the same things
- Yannis Smaragdakis19 talks
- Xiaohong Chen4 talks
- Mooly Sagiv18 talks
- Jon Stephens4 talks
- François René Rideau10 talks
- Andrew Poelstra16 talks
| title | conference | date |
|---|---|---|
| Fireside Chat | Pragma Buenos Aires 2025 | 2025-11-20 |
Pi Squared builds a two-part stack: a proof of proof pipeline that turns program execution into a mathematical proof via the K framework and a settlement layer… | ||
| The Future of Web3 Is Not Blockchain | Pragma Cannes 2025 | 2025-07-03 |
Argues that total ordering is the bottleneck and that payments, computations and asset transfers can settle as independent claims with proofs using a… | ||
| Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic | OOPSLA 2020 | 2020-11-15 |
A unified proof framework uses matching logic as a base to build automated provers for multiple logics, implementing 11 generic rules (including LFP based on… | ||
| A General Approach to Define Binders Using Matching Logic | ICFP 2020 | 2020-08-23 |
Defines binders by using matching logic’s built‑in exists to form the graph set [X]E and then a constructor to build the binder term, encapsulated as the… | ||
| Matching Logic: Foundation of the K Framework | CPP 2020 | 2020-01-20 |
One formal semantics drives interpreters, verifiers and model checkers: a 5,000‑rule C11 semantics with a >120‑cell configuration compiles to LLVM and yields a… | ||
| nothing matches | ||