solutions.basics

• Basics of Iris
  • Introduction
  • Iris in Coq
  • Basic Separation Logic

solutions.pure

• Pure Propositions

solutions.lang

• HeapLang
  • Introduction
  • The HeapLang Interpreter (Optional)
  • Pure Constructs
  • References
  • Concurrency

solutions.specifications

• Specifications
  • Introduction
  • Weakest Precondition
  • Resources
  • Composing Programs and Proofs
  • Hoare Triples
  • Concurrency

solutions.persistently

• Persistently
  • Introduction
  • Proving Persistency
  • Examples of Persistent Propositions

solutions.linked_lists

• Case Study: Linked Lists

solutions.later

• Later
  • Basics
  • Tying Later to Program Steps
  • Löb Induction

solutions.arrays

• Arrays
  • Copy
  • Increment
  • Reverse

solutions.gr_predicates

• Guarded Recursive Predicates

solutions.resource_algebra

• Resource Algebra
  • Introduction
  • Basic Concepts of Resource Algebra
  • Example Resource Algebra
  • Ghost State
  • Accessing Resource Algebras in Coq

solutions.invariants

• Invariants
  • A Motivating Example
  • Introduction to Invariants
  • A Motivating Example – Take Two
  • Another Example

solutions.timeless

• Timeless Propositions
  • Definition and Uses
  • Timeless Propositions and Invariants

solutions.structured_conc

• Structured Concurrency
  • Introduction
  • The Fork Construct
  • The Spawn Construct
  • The Par Construct

solutions.counter

• Case Study: Counter
  • Implementation
  • Defining a Representation Predicate for the Counter
  • Properties of the Authoritative RA with MaxNat
  • Proving the Counter Specification
  • A Simple Counter Client
  • A Stronger Counter Specification

solutions.spin_lock

• Case Study: Spin Lock
  • Implementation
  • Representation Predicates
  • Specifications
  • Example Client

solutions.ticket_lock

• Case Study: Ticket Lock
  • Implementation
  • Representation Predicates
  • Specifications

solutions.adequacy

• Adequacy

solutions.merge_sort

• Case Study: Merge Sort
  • Implementation
  • Specifications

solutions.custom_ra

• Custom Resource Algebra
  • A Motivating Example
  • Defining the State RA
  • Properties of State
  • Using the State RA in Proofs

solutions.ofe

• Ordered Families of Equivalences (OFE)

exercises.basics

• Basics of Iris
  • Introduction
  • Iris in Coq
  • Basic Separation Logic

exercises.pure

• Pure Propositions

exercises.lang

• HeapLang
  • Introduction
  • The HeapLang Interpreter (Optional)
  • Pure Constructs
  • References
  • Concurrency

exercises.specifications

• Specifications
  • Introduction
  • Weakest Precondition
  • Resources
  • Composing Programs and Proofs
  • Hoare Triples
  • Concurrency

exercises.persistently

• Persistently
  • Introduction
  • Proving Persistency
  • Examples of Persistent Propositions

exercises.linked_lists

• Case Study: Linked Lists

exercises.later

• Later
  • Basics
  • Tying Later to Program Steps
  • Löb Induction

exercises.arrays

• Arrays
  • Copy
  • Increment
  • Reverse

exercises.gr_predicates

• Guarded Recursive Predicates

exercises.resource_algebra

• Resource Algebra
  • Introduction
  • Basic Concepts of Resource Algebra
  • Example Resource Algebra
  • Ghost State
  • Accessing Resource Algebras in Coq

exercises.invariants

• Invariants
  • A Motivating Example
  • Introduction to Invariants
  • A Motivating Example – Take Two
  • Another Example

exercises.timeless

• Timeless Propositions
  • Definition and Uses
  • Timeless Propositions and Invariants

exercises.structured_conc

• Structured Concurrency
  • Introduction
  • The Fork Construct
  • The Spawn Construct
  • The Par Construct

exercises.counter

• Case Study: Counter
  • Implementation
  • Defining a Representation Predicate for the Counter
  • Properties of the Authoritative RA with MaxNat
  • Proving the Counter Specification
  • A Simple Counter Client
  • A Stronger Counter Specification

exercises.spin_lock

• Case Study: Spin Lock
  • Implementation
  • Representation Predicates
  • Specifications
  • Example Client

exercises.ticket_lock

• Case Study: Ticket Lock
  • Implementation
  • Representation Predicates
  • Specifications

exercises.adequacy

• Adequacy

exercises.merge_sort

• Case Study: Merge Sort
  • Implementation
  • Specifications

exercises.custom_ra

• Custom Resource Algebra
  • A Motivating Example
  • Defining the State RA
  • Properties of State
  • Using the State RA in Proofs

exercises.ofe

• Ordered Families of Equivalences (OFE)