Types & Choreographies
Liquidity Analysis in Resource-Aware Programming
Presenter: Cosimo Laneve
Session Chair: EmÃlio Tuosto
Liquidity is a sensible security property of programs man- aging resources that pinpoints those programs not freezing any resource forever. We consider a simple stateful language whose resources are as- sets (digital currencies, non fungible tokens, etc.). Then we define a type system that tracks in a symbolic way the input-output behaviour of func- tions with respect to assets. By composing the input-output behaviours we derive liquidity types of computations that we use for designing two algorithms that verify two liquidity properties. We also demonstrate the correctness of the algorithms.