notes

Outline:

Introduction

  bla bla type theory
  what's the problem (reduction with ill-typed terms)
  solution

  our contributions:
  - practical type checking algorithm
  - definitions by pattern matching (new kinds of neutral terms)

  what are meta variables used for?
  - user interaction
  - proof search
  - implicit arguments	<-- our focus

The Core theory

  what should the core system contain?
  - definitions by pattern matching, kept very abstract

  (mutual) recursion?
  - no mutual recursion

  no type checking, just typing rules
  no proofs
  (what properties can we assume?)

Type checking with meta variables

  Introducing meta variables

    top-level things (necessary since we don't have explicit substitutions)

    what do we want them for: implicit arguments

  Examples

    what happens to the conversion rule?

  Rules

    revisit examples

  Proofs

    soundness of convertibility checking

    safety (simple proof)

    soundness (follows from safety)

      if we solve all constraints we get something well-typed in Core

    completeness (ignore, or mention briefly)

    how much detail? only the interesting cases.
    at least we have to do the proofs ourselves!

Related work

Conclusions

Notes
-----

structure of properties:

  - safety: we only compute with well-typed terms
  - soundness: solving constraints gives a well-typed result

first prove everything without constraint simplification
then prove soundness of simplification
then we should have a general soundness result

How to deal with the invariants?
- Can we prove them once and for all?
- Make them implicit?
- Write them out everywhere?
Wait... we need the type safety theorem to ensure the invariants!

Hmm.. so I guess we need to prove everything at once. Painful!
Ok, not that bad.

Soundness of Constraints

  what do we want to say?

  constraint simplification is a signature extension operator

Think about why exactly we don't prove consistency at the same time as soundness
(we need soundness in the consistency proof). It's stated explicitly so forget
this.

Now what?
---------

Examples
  - where?
  - which?

F ? example:
  
  F : B -> Set
  F true  = N
  F false = B

  not : B -> B
  not true  = false
  not false = true

  h : ((x : F _) -> F (not x)) -> N
  h g = g zero

delta-delta example:

  lam : (X,Y:Set) -> (X -> Y) -> (X => Y)
  app : (X,Y:Set) -> (X => Y) -> (X -> Y)
  app X Y (lam f) = f

  delta : ?A
  delta = lam ?X ?Y (\x -> app ?Z ?W x x)

  loop = app ?B ?C delta delta


more examples? what would they illustrate?

some non-problematic cases (simple examples)
  id : (A:Set) -> A -> A
  id ? zero

scope example!

both examples above need pattern matching

 vim: sts=2 sw=2 tw=80