9 citations · 9 across the 1 of their papers we have counts for
3 papers
cs.LO2017★ 9 cited
Fibred Computational Effects
Danel Ahman
Dependent types provide a lightweight and modular means to integrate programming and formal program verification. In particular, the types of programs written in dependently typed…
cs.PL2017
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu +3
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the…
cs.LO2016
Directed Containers as Categories
Danel Ahman, Tarmo Uustalu
Directed containers make explicit the additional structure of those containers whose set functor interpretation carries a comonad structure. The data and laws of a directed contain…