Danel Ahman

40 papers A* 1A 2B 6Journal 26Unranked 4
YearRankTypeTitle / Venue / Authors
2026 J jnl
Misquoted No More: Securely Extracting F* Programs with IO.
CoRR
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter
2026 J jnl
Sheaves as oracle computations.
CoRR
Danel Ahman, Andrej Bauer
2026 J jnl
Strong Normalisation for Asynchronous Effects.
CoRR
Danel Ahman, Ilja Sobolev
2025 J jnl
A simple formalization of alpha-equivalence.
CoRR
Kalmer Apinis, Danel Ahman
2025 J jnl
Comodule representations of second-order functionals.
J. Log. Algebraic Methods Program.
Danel Ahman, Andrej Bauer
2025 J jnl
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F.
CoRR
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
2025 J jnl
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F.
Proc. ACM Program. Lang.
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
2024 J jnl
Comodule Representations of Second-Order Functionals.
CoRR
Danel Ahman, Andrej Bauer
2024 J jnl
Higher-Order Asynchronous Effects.
Log. Methods Comput. Sci.
Danel Ahman, Matija Pretnar
2023 J jnl
Higher-Order Asynchronous Effects.
CoRR
Danel Ahman, Matija Pretnar
2023 B conf
When Programs Have to Watch Paint Dry.
FoSSaCS
Danel Ahman
2022 J jnl
When programs have to watch paint dry.
CoRR
Danel Ahman
2021 J jnl
Asynchronous effects.
Proc. ACM Program. Lang.
Danel Ahman, Matija Pretnar
2021 J jnl
Scalable Handling of Effects (Dagstuhl Seminar 21292).
Dagstuhl Reports
Danel Ahman, Amal Ahmed, Sam Lindley, Andreas Rossberg
2021 J jnl
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs.
CoRR
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
2020 J jnl
Asynchronous effects.
CoRR
Danel Ahman, Matija Pretnar
2020 A conf
Runners in Action.
ESOP
Danel Ahman, Andrej Bauer
2020 J jnl
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs.
Proc. ACM Program. Lang.
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
2019 B conf
Decomposing Comonad Morphisms.
CALCO
Danel Ahman, Tarmo Uustalu
2019 J jnl
Dijkstra Monads for All.
CoRR
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
2019 J jnl
Dijkstra monads for all.
Proc. ACM Program. Lang.
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
2019 A conf
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
ESOP
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
2019 J jnl
Runners in action.
CoRR
Danel Ahman, Andrej Bauer
2018 J jnl
Handling fibred algebraic effects.
Proc. ACM Program. Lang.
Danel Ahman
2018 J jnl
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
2018 J jnl
Recalling a witness: foundations and applications of monotonic state.
Proc. ACM Program. Lang.
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2017 A* conf
Dijkstra monads for free.
POPL
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2017 J jnl
Fibred Computational Effects.
CoRR
Danel Ahman
2017 — —
Fibred computational effects
Danel Ahman
2017 J jnl
Recalling a Witness: Foundations and Applications of Monotonic State.
CoRR
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2017 — conf
Taking Updates Seriously.
BX@ETAPS
Danel Ahman, Tarmo Uustalu
2016 B conf
Dependent Types and Fibred Computational Effects.
FoSSaCS
Danel Ahman, Neil Ghani, Gordon D. Plotkin
2016 J jnl
Dijkstra Monads for Free.
CoRR
Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2016 — conf
Directed Containers as Categories.
MSFP
Danel Ahman, Tarmo Uustalu
2014 B conf
Coalgebraic Update Lenses.
MFPS
Danel Ahman, Tarmo Uustalu
2014 J jnl
When is a container a comonad?
Log. Methods Comput. Sci.
Danel Ahman, James Chapman, Tarmo Uustalu
2013 B conf
Normalization by Evaluation and Algebraic Effects.
MFPS
Danel Ahman, Sam Staton
2013 — conf
Update Monads: Cointerpreting Directed Containers.
TYPES
Danel Ahman, Tarmo Uustalu
2012 — conf
Constraint-Based Heuristic On-line Test Generation from Non-deterministic I/O EFSMs
MBT
Danel Ahman, Marko Kääramees
2012 B conf
When Is a Container a Comonad?
FoSSaCS
Danel Ahman, James Chapman, Tarmo Uustalu