A Hoare-Logic Style Refinement Types Formalisation
summary
Presents a Hoare-triple style formalisation of refinement types implemented in Agda that interprets object terms shallowly and uses Agda’s type theory as the logic. Targets a simply-typed lambda calculus with products and first-order functions, computes weakest preconditions to deterministically infer preconditions from a user postcondition, and emits a verification condition generator that aggregates proof obligations for SMT or manual discharge. Proves soundness and completeness of the refinement typing and WP machinery and shows how loop annotations are validated.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:21Refinement Type Systems
- 3:12Dependency
- 4:44Hoare Logic
- 7:08Formalising Refinement Types
- 8:26Agda Formalisation
- 10:13Backwards Reasoning Weakest Precondition (wp)
- 13:00Function Contracts
- 14:36Future Work
related talks
29mExplicit Refinement Types
46mRefinement Types from Light to Deep Verification
19mType Inference Logics
34mLiquid Haskell: Verification with Refinement Types
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
21mRefinement Type Refutations
45mLogic Meta Programming for Functional Languages