9 citations · 9 across the 8 of their papers we have counts for
Showing 2017Show all
2 papers · 1 filter
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…