[Agda] Fixpoint in Agda

Marco Vassena vassena at chalmers.se
Wed Jul 19 21:08:43 CEST 2017


Hello,

Does Agda currently support fixpoint computations?

I am particularly interested in computing the least fixpoint via Ascending Chain Condition (ACC),
for the purpose of verified program analysis.

Could you point me to existing work, if there is any?

Best,
Marco Vassena


More information about the Agda mailing list