Takeshi Tsukada
where else to find them
no profile links on file
what they talk about
all 6 in the filters
where they keep going back
- POPL4 editions2022–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
all 8 in the filters
on a stage with
all 22 in the filters
who talks about the same things
- Hiroshi Unno18 talks
- Sharon Shoham13 talks
- Taro Sekiyama12 talks
- Naoki Kobayashi17 talks
- Thomas Reps20 talks
- Ranjit Jhala19 talks
| title | conference | date |
|---|---|---|
| Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification | PLDI 2026 | 2026-06-15 |
Presents a concrete criterion that turns uniqueness of least fixed points into a usable lower-bound proof: existence of a U-ranking supermartingale plus a… | ||
| Nola: Later-Free Ghost State for Verifying Termination in Iris | PLDI 2025 | 2025-06-16 |
Nola presents a concrete method to remove Iris’s obstructive later modality by encoding shared state as syntactic SL formulas and giving them a separate… | ||
| A Primal-Dual Perspective on Program Verification Algorithms | POPL 2025 | 2025-01-19 |
Presents a unified algorithmic framework that generalizes Lagrangians to discrete domains (powersets, predicates, ranking functions) and runs an abstract… | ||
| Inductive Approach to Spacer | PLDI 2024 | 2024-06-24 |
Presents a Spacer-like CHC solver derived by structural induction that replaces global quantifier elimination with an iterative, lazy use of model-based… | ||
| Quantum Controlled Measurements via Program Transformation | PLanQC 2024 | 2024-01-20 |
Proposes a program transformation that defers measurements from inside quantum conditionals to the outside, turning programs with mid-circuit measurements into… | ||
| Enriched Presheaf Model of Quantum FPC | POPL 2024 | 2024-01-14 |
Extends Selinger’s superoperator model to higher-order programs by building modules over superoperators (equivalently enriched presheaves) and carving a… | ||
| Optimal CHC Solving via Termination Proofs | POPL 2023 | 2023-01-15 |
Presents a new optimality checker that reduces CHC maximality to program termination, encodes termination-argument synthesis (angelic strategy and… | ||
| HFL(Z) Validity Checking for Automated Program Verification | POPL 2023 | 2023-01-15 |
Proposes an automated validity checker for HFL(Z) formulas that encodes higher-order program verification (termination, nontermination, fair variants… | ||
| A New Refinement Type System for Automated nu-HFLZ Validity Checkin | SPLASH 2022 | 2022-12-05 |
A refinement type system targets validity checking for a fragment of vHFLZ (no least fixpoints) and produces template-based constraints that are solved to… | ||
| Termination Analysis for the pi-Calculus by Reduction to Sequential Program Termination | SPLASH 2022 | 2022-12-05 |
Proposes an automated reduction that translates pi-calculus processes into sequential C programs so termination of the C program implies termination of the… | ||
| Software Model-Checking as Cyclic-Proof Search | SPLASH 2022 | 2022-12-05 |
Claims that many software model-checking procedures are just proof-search strategies for a cyclic proof system and gives a worked mapping: symbolic execution… | ||
| Software Model-Checking as Cyclic-Proof Search | POPL 2022 | 2022-01-16 |
Claims that many software model-checking algorithms are exactly proof-search strategies for a cyclic proof system, so a single logical framework reconstructs… | ||
| Termination Analysis for the \$\pi\$-Calculus by Reduction to Sequential Program Termination | APLAS 2021 | 2021-10-17 |
Proposes an automated reduction that translates π-calculus to C so termination of the sequential program implies termination of the original process, and… | ||
| Coq to C Translation with Partial Evaluation + Counterexample Generation | PEPM 2021 | 2021-01-18 |
Builds a verified Coq-to-C code generator that uses a custom codogen plugin and a partial-evaluation pipeline to monomorphize polymorphic/dependent functions… | ||
| Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking | SAS 2020 | 2020-11-18 |
Proposes an algorithm that combines νHFL(ℤ) predicate abstraction with predicate abstraction and CEGAR to decide higher‑order CHC/νHFL(ℤ) validity, implements… | ||
| Signature restriction for polymorphic algebraic effects | ICFP 2020 | 2020-08-23 |
Proposes signature restriction on effect interfaces: require each bound type variable to occur only strictly positively in argument positions and only… | ||
| nothing matches | ||