Taro Sekiyama
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- POPL3 editions2023–2025
- OOPSLA2 editions2024–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
all 7 in the filters
on a stage with
all 12 in the filters
who talks about the same things
- Hiroshi Unno18 talks
- Ugo Dal Lago14 talks
- Takeshi Tsukada16 talks
- Tachio Terauchi4 talks
- Atsushi Igarashi5 talks
- Oliver Bračevac9 talks
| title | conference | date |
|---|---|---|
| On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs | OOPSLA 2025 | 2025-10-16 |
Claims decidability for a nontrivial fragment of effectful higher-order programs by introducing polymorphic answer-type □ and a type system that allows… | ||
| Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning | IWACO 2025 | 2025-10-14 |
Type system enriches substructural resource types with a resettable timer that bounds progress through transition-system states and forces resources to reach… | ||
| Thrust: A Prophecy-Based Refinement Type System for Rust | PLDI 2025 | 2025-06-16 |
A new Rust verifier called Thrust implements a dependent refinement type system plus an inference pipeline that emits Constrained Horn Clauses to a CHC solver… | ||
| Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order(…) | POPL 2025 | 2025-01-19 |
Proposes algebraic temporal effects: an axiomatized effect algebra plus an R modality for guarded recursive types that stratifies infinite behavior, an effect… | ||
| Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification | OOPSLA 2024 | 2024-10-20 |
Claims decidability for higher-order model checking of programs with algebraic effect handlers by statically bounding the number of simultaneously active… | ||
| Space-Efficient Polymorphic Gradual Typing, Mostly Parametric | PLDI 2024 | 2024-06-24 |
Claim: space-efficient gradual typing becomes possible when polymorphism is restricted to mostly parametric, meaning parametricity is enforced only for… | ||
| Answer Refinement Modification: Refinement Type System for Algebraic Effects and... | POPL 2024 | 2024-01-14 |
Proposes a refinement type system that tracks how delimited-continuation effects change return types via answer refinement modification, formalizes ATM/ARM… | ||
| Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-a... | POPL 2023 | 2023-01-15 |
Extends a temporal type-and-effect system to handle delimited continuations (shift0/reset0) by tracking how continuations change the observable trace — the key… | ||
| Toward Neural-Network-Guided Program Synthesis and Verification | SAS 2021 | 2021-10-17 |
Proposes NeuGuS, a gray-box method that trains neural nets (four-layer; sometimes three-layer) then extracts inequalities from weights/biases to build Boolean… | ||
| Is Space-Efficient Polymorphic Gradual Typing Possible? | Scheme 2021 | 2021-08-27 |
Argument shows that preserving parametric polymorphism plus standard gradual-typing guarantees prevents a generic space-efficient implementation: a formal… | ||
| 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 | ||