Ugo Dal Lago
where else to find them
no profile links on file
what they talk about
where they keep going back
all 5 in the filters
on a stage with
all 14 in the filters
who talks about the same things
- Taro Sekiyama12 talks
- Hiroshi Unno18 talks
- Deepak Garg18 talks
- Oliver Bračevac9 talks
- Magnus Madsen11 talks
- Lars Birkedal35 talks
| title | conference | date |
|---|---|---|
| On Circuit Description Languages, Indexed Monads, and Resource Analysis | POPL 2026 | 2026-01-11 |
Presents a monad-based denotational semantics for Proto-Quipper variants that cleanly separates returned values from the circuits a term generates, using a… | ||
| 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… | ||
| Towards Quantum Multiparty Session Types | PLanQC 2025 | 2025-01-25 |
Proposes Quantum MPSTs that extend multiparty session types with linearity and quantum primitives, implements an operational semantics as a labeled transition… | ||
| Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages | POPL 2025 | 2025-01-19 |
Introduces a type-and-effect system for Quipper that produces parametric upper bounds on circuit size (width, gate count, and wire-level depth) by combining… | ||
| Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abs... | PLanQC 2024 | 2024-01-20 |
Proto-Quipper-R implements a linear dependent type-and-effect system that produces parametric upper bounds on circuit width (indices are arithmetic expressions… | ||
| On Interaction, Efficiency, and Reversibility | GALOP 2024 | 2024-01-14 |
Claim: the Interaction Abstract Machine (IAM) fails the usual invariance thesis — it is not invariant for time or space under natural encodings of Turing… | ||
| On Model-Checking Higher-Order Effectful Programs | POPL 2024 | 2024-01-14 |
Paper shows higher-order effectful programs map to ordinary higher-order recursion schemes via a CPS transformation and recovers classic model-checking… | ||
| Multi Types and Reasonable Space | ICFP 2022 | 2022-09-11 |
Claims a concrete machine, Space KAM, is a reasonable space cost model for the lambda calculus (linear overhead vs. Turing/RAM) and handles logarithmic-space… | ||
| On Feller Continuity and Full Abstraction | ICFP 2022 | 2022-09-11 |
Shows that in a call-by-value higher-order lambda calculus with sampling and only continuous real-valued primitives, Feller-continuity on the induced labelled… | ||
| Effectful Program Distancing | POPL 2022 | 2022-01-16 |
Proposes a semantic framework that extends differential logical relations to effectful higher-order languages and proves a fundamental lemma that yields… | ||
| A Relational Theory of Effects and Coeffects | POPL 2022 | 2022-01-16 |
Paper gives an operational, relational framework for higher-order languages with graded modal types and algebraic effects, using a monadic semantics (Maybe… | ||
| Intersection Types and (Positive) Almost-Sure Termination | POPL 2021 | 2021-01-17 |
Intersection types exactly characterize two probabilistic termination notions: the probability of convergence equals the least upper bound of norms of certain… | ||
| The (In)Efficiency of Interaction | POPL 2021 | 2021-01-17 |
Compares four token-based abstract machines and proves precise time gaps: YAM (geometry of interaction) can be exponentially slower than Curien’s environment… | ||
| nothing matches | ||