RefinementTypes.Syntax

• Syntax (Figure 5)
  • Binary operations
  • Types and terms
  • Values
  • Custom induction principle for values
  • Decidable equality for types and terms

RefinementTypes.Eval

• Evaluation (Figures 6 and 7)
  • Binary operations
  • Loops
  • The interpreter (Figure 7)

RefinementTypes.Subst

• De Bruijn Renaming and Substitution
  • Infrastructure
  • Renaming
  • Substitution helpers
  • Substitution
  • Iterated up
  • Derived operations

RefinementTypes.SubstLemmas

• Substitution Lemmas
  • Renaming extensionality
  • Up extensionality helpers
  • Substitution extensionality
  • Renaming identity
  • Substitution identity
  • Renaming-substitution connection
  • Renaming composition
  • Substitution after renaming
  • Renaming after substitution
  • Substitution composition
  • Iterated up_tm_tm lemmas
  • Term-only shift substitution

RefinementTypes.SubstExamples

• Substitution Tests
  • Renaming examples
  • Substitution examples
  • ty_subst examples
  • Identity substitution
  • Cross-sort independence

RefinementTypes.Tactics

• Tactics

RefinementTypes.ListLemmas

• List Lemmas

RefinementTypes.EvalLemmas

• Evaluation Lemmas
  • Fuel monotonicity for run_loop
  • Type preservation for run_loop
  • Fuel monotonicity
  • Evaluation of binary operations

RefinementTypes.EvalShiftLemmas

• Evaluation Weakening (Lemma 3.7)
  • Weakening compatibility relation
  • Weakening simulation (Lemma 3.7)
  • Corollaries: shifting the environment

RefinementTypes.EvalSubstLemmas

• Evaluation Substitution (§3.6)
  • Substitution compatibility relation
  • Substitution simulation
  • Corollaries: substituting a variable for an environment entry

RefinementTypes.EvalTypeErasure

• Type Erasure

RefinementTypes.Interp

• Interpretation (Figure 8)
  • Semantic types
  • Term interpretation E⟦.⟧
  • Value interpretation components
  • Value interpretation V⟦.⟧
  • Extensionality

RefinementTypes.InterpShiftLemmas

• Interpretation Weakening (Lemmas 3.3 and 3.5)
  • Predicates: eval_to_true is invariant under type erasure
  • Term weakening (Lemma 3.3)
  • Type weakening (Lemma 3.5)

RefinementTypes.InterpSubstLemmas

• Interpretation Substitution (Lemmas 3.4 and 3.6)
  • Term substitution (Lemma 3.4)
  • Type substitution (Lemma 3.6)
  • The generalized type substitution function.

RefinementTypes.Wf

• Well-Formed Environments (Figure 8)
  • Term bindings
  • Equality facts
  • Type variable bounds

RefinementTypes.WfLemmas

• Well-Formedness Lemmas
  • Lemmas about wf_env
  • Lemmas about wf_facts
  • Lemmas about wf_benv

RefinementTypes.Positivity

• Strict Positivity (Figure 11)

RefinementTypes.PositivityLemmas

• Positivity Lemmas (Lemmas 3.9 and 3.10)
  • term_has_semtype is monotone in its predicate
  • Interpretation is independent of absent type variables
  • Monotonicity (Lemma 3.9)
  • Distribution (Lemma 3.10)
  • Monotonicity of interp_mu in F

RefinementTypes.Avoid

• Avoidance (§3.4)
  • Occurrence check
  • The avoidance function

RefinementTypes.AvoidLemmas

• Avoidance Soundness (Lemma 3.8)
  • Avoidance preserves positivity
  • Avoidance soundness (Lemma 3.8)
  • Avoided types are closed under the avoided variable

RefinementTypes.FirstOrder

• First-Order Types (§3.4)

RefinementTypes.FirstOrderLemmas

• Lemmas about First-Order Types

RefinementTypes.SemanticImplies

• Semantic Implication (Figure 8)

RefinementTypes.SemanticSubtyping

• Semantic Subtyping (§3.5, Figures 8 and 10)
  • The judgment (Figure 8)
  • Reflexivity and transitivity
  • Function and universal type subtyping rules
  • Sigma type subtyping rule
  • Union type subtyping rules
  • Intersection type subtyping rules
  • Refinement type subtyping rules
  • Top and Bottom type subtyping rules
  • Type variable bound extraction rules
  • Recursive type subtyping rules

RefinementTypes.SemanticTyping

• Semantic Typing (§3.4, Figures 8 and 9)
  • The judgment (Figure 8)
  • Constants
  • Variables, functions, and polymorphism
  • Let bindings and control flow
  • Selfification and subsumption
  • Pairs and sums

RefinementTypes.SyntacticSubtyping

• Syntactic Subtyping (Figure 10)

RefinementTypes.SyntacticTyping

• Syntactic Typing (Figure 9)

RefinementTypes.Adequacy

• Adequacy (Theorems 3.1 and 3.2)

RefinementTypes.AlgorithmicTyping

• Algorithmic Typing
  • Algorithmic typing

RefinementTypes.Examples

• Example: maximum
  • Type abbreviations
  • Types and terms
  • Evaluation tests
  • Subtyping derivations
  • Typing derivation

RefinementTypes.ExamplesCollect

• Example: collect (Figure 4)
  • Type abbreviations
  • Type of collect
  • Term: collect
  • Evaluation tests

RefinementTypes.ExamplesPartialSoundness

• Partial Correctness and Divergent Predicates (§2.3, Lemmas 2.1–2.3)
  • 0a. Bot and {T | false} have the same interpretation, for any T.
  • 0b. Unit and {Unit | true} have the same interpretation.
  • 1a. No value inhabits Bot.
  • 1b. No converging term has type Bot.
  • 2. {Unit | true} and {Unit | diverge} have the same interpretation.
  • 3a. {Unit | diverge} is not a semantic subtype of {Unit | false}
  • 3b. {Unit | diverge && false} is not a subtype of {Unit | false}.
  • Helper: evaluation of t && b in terms of the evaluation of t.
  • 4. Entailment Γ ⊨ t && true ⟹ t holds for arbitrary t
  • 5a. Entailment Γ ⊨ t && false ⟹ false fails for diverging t.
  • 5b. Entailment Γ ⊨ t && false ⟹ false holds when t terminates
  • 6. {x: A | diverge} and {x: A | true} have the same interpretation,
  • 7. No converging term has type {x: A | false}, for any A