Search

• < Previous
• 1
• Next >

---

Amortised Resource Analysis with Separation Logic

Robert Atkey.

Type-based amortised resource analysis following Hofmann and Jost---where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline---have been successful in providing concrete resource bounds for functional programs, with&nbsp;[&hellip;]

---

Refining Inductive Types

Robert Atkey ; Patricia Johann ; Neil Ghani.

Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists&nbsp;[&hellip;]

---