# Formalized Metatheory in F*

#### Cătălin Hriţcu (Inria Paris)

Type Systems for Security Verification Lecture

Saarland University

Monday, 23 March 2015

## Last Friday

• Small-step reduction
• Simple types
• arithmetic and boolean expressions; While language
• Simply Typed -calculus (STLC; call-by-value)
• Style:
• named representation of terms
• everything pure and executable; extrinsic style proofs
• Homework:
• extending STLC formalization with integers, let rec, pairs
• optional: subtyping (quite challenging in this style)

## Today

• Another formalization of STLC
• strong reduction (TAPL 5.1)
• nameless representation of terms (TAPL 6)
• parallel substitution
• : kinds and type-level computation (TAPL 29 & 30)
• Style:
• mixing executable code and inductive relations
• mixing extrinsic and constructive style proofs
• Homework: extend STLC formalization
• with subtyping (TAPL 15) and simple state (While)
• bonus points: do real references (TAPL 13)
• extra bonus points: do any of these for

## Strong reduction

((fun x:t -> e1) e2) ~> e1[e2/x]  [S-Beta]e1 ~> e1'------------------- [S-App1](e1 e2) ~> (e1' e2)e2 ~> e2'------------------- [S-App2](e1 e2) ~> (e1 e2')e ~> e'--------------------------------- [S-Lam](fun x:t -> e) ~> (fun x:t -> e')

non-deterministic (but confluent) evaluation strategy
(aka. full beta-reduction): any redex can reduce at any time

## Nameless representation of terms

• de Bruijn indices; following TAPL 6

## : Type Operators and Kinds

• following TAPL 29 & 30
• we can see (list t) as an application
• and list as a type constructor
• Type operators:
• fun a : Type -> list a
• id = (fun a : Type -> a)
• Formally, we extend types with another -calculus:
• t ::= t1 -> t2 | a | (fun a:k -> t) | t1 t2

## Primitive type operators in F*

         and : Type -> Type -> Type          or : Type -> Type -> Type         not : Type -> Type        impl : Type -> Type -> Type      forall : a:Type -> (a -> Type) -> Type          eq : a:Type -> a -> a -> Type    precedes : a:Type -> a -> a -> Type        eq_k : a1:k -> a2:k -> Type    forall_k : (a:k -> Type) -> Type

## Predicate transformers (wp)

kind PURE.Pre = Typekind PURE.Post (a:Type) = a -> Typekind PURE.WP (a:Type) = Post a -> Pretype PURE.return (a:Type) (x:a) : PURE.WP a = fun p -> p xtype PURE.bind (a:Type) (wp1:PURE.WP a) (wp2:a->PURE.WP b) : PURE.WP b =    fun p -> wp1 (fun x -> wp2 x p)

## Type-level computation

• The following types are equivalent:
• nat -> bool
• id nat -> bool
• nat -> id bool
• id (nat -> bool)
• id nat -> id bool
• id (id (id nat -> bool))
• Generally
• ((fun a : k -> t1) t2) t1[t2/a]
• Type conversion rule

## Kinds

• Lambdas and applications at type level can be bogus
• Meaningless type expressions:
• (bool nat) doesn't make more sense than (true 6)
• Kinds: “the types of types”
• Simple kinds (STLC one level up)
• k ::= Type | k1 -> k2
• Type: (aka. ) the kind of proper types (like bool, bool -> bool)
• Type -> Type: type operators (like list and id)
• Type -> Type -> Type: two-argument type operators (like and)
• (Type -> Type) -> Type: higher-order operators (like forall)

## Well-typed expressions assigned types

Functions get arrow types Non-sense expressions get no type

## Type operators get arrow kinds

And non-sense types get no kind

## Kinding rules (remember STLC?)

    G |- ok    ------------- [K-Var]    G |- a : G(a)    G, a:k |- t : k'    --------------------------------- [K-Abs]    G |- (fun (a:k) -> t) : (k -> k')    G |- t1 : k -> k'    G |- t2 : k    -------------------------------- [K-App]    G |- t1 t2 : k'    G |- t1 : Type      G |- t2 : Type    ---------------------------------- [K-Arr]    G |- t1 -> t2 : Type

## Type equivalence (conversion)

 ((fun a : k -> t1) t2) t1[t2/a] [Eq-Beta]t t'-------------------------------- [Eq-Lam](fun a:k -> t) (fun a:k -> t')t1 t1' t2 t2'--------------------- [Eq-App](t1 t2) (t1' t2')t1 t1' t2 t2'--------------------- [Eq-Arr](t1->t2) (t1'->t2') t t [Eq-Refl]t s----- [Eq-Symm]s tt1 t2 t2 t3------------------- [Eq-Tran]t1 t3

## Typing rules for

 G |- ok------------- [T-Var]G |- x : G(x)G, x:t |- e : t' G |- t1 : Type---------------------------------- [T-Abs]G |- (fun (x:t) -> e) : (t -> t')G |- e1 : t -> t' G |- e2 : t-------------------------------- [T-App]G |- e1 e2 : t'G |- e : t t t'------------------- [T-Conv]G |- e : t' . |- ok [G-Empty]G |- t : Type x not in dom G------------------------------- [G-Type]G, x:t |- oka not in dom G-------------- [G-Kind]G, a:k |- ok

= STLC with type operators

## Projects

• How many people? How many teams?

• Anyone who already found a potential topic?

• We also have a long list of potential topics

• from which you can choose based on your interests