ynot march 2007

Information about ynot march 2007

Published on June 17, 2007

Author: Sabatini

Source: authorstream.com

Content

Y0 Y-not Y-knot Y-naught?:  Y0 Y-not Y-knot Y-naught? Greg Morrisett with Aleks N., Ryan W., Paul G., Rasmus P., Lars B. ESC, JML, Spec#, …:  ESC, JML, Spec#, … Need a different spec language: 'pure' boolean expressions: length(x)==42 'modeling' types (e.g., pure lists, sets, …) If the implementation is pure, can’t use it in the specs! x.f versus \old(x.f) What if Simplify can’t prove something? Ignore (e.g., arith, modifies clause): unsound Rewrite code? Weaken spec? Not really modular: can’t write 'app' or 'map' DML, ATS, Omega, …:  DML, ATS, Omega, … Introduce different spec language. Again, a separate 'pure' language To capture all properties of lists, you’d have to index them with well, lists. Can’t talk about properties of effectful computations (or limited capacity). ATS can build proofs, but it’s awkward. Coq, PRL, Isabelle, …:  Coq, PRL, Isabelle, … Ynot starts with Coq as the basic language: [co]inductive definitions, h.o. functions, polymorphism, h.o. predicates, proofs, … Strong support for modularity e.g., can package up and abstract over terms, types, predicates, proofs, in a uniform fashion. can prove that, e.g., append is associative and rev(rev(x)) = x, etc. after defining it. But huge drawback: No effects (non-term, IO, state, recursive types, etc.) Not a strong phase separation Quick Coq:  Quick Coq Set : (think * in Haskell) nat, bool, functions from sets to sets, … inductive set definitions (e.g., list) co-inductive set definitions (e.g., stream) Prop : Think of nat-andgt;Prop as a subset of nat. Equality, /\, \/, etc. [co-]inductive definitions (e.g., judgments) Refinement:  Refinement Can form mixed products andamp; sums {n:nat | n andgt;= 42} is a pair of a nat and a proof that this nat is andgt;= 42. Array subscript: forall (A:Set)(n:nat) (v:vector n A) (j:nat), (j andlt; n) -andgt; A Can extract Ocaml or Haskell code. 'erase' Prop objects (really, replace with unit). Purity:  Purity We want to pull the Curry-Howard isomorphism to represent a proof of Prop P as a term with type P. Reduce proof-checking to type-checking. Should be no term with type False. If we added recursive functions, recursive types, exceptions, or refs, we could code up a term of type False. So everyone forgoes these 'features' in their type theory. Coq Demo:  Coq Demo A few examples… Ynot and HTT:  Ynot and HTT We add a new type constructor, IO A As in Haskell, encapsulate effectful computations. We’re not pretending that IO False is a proof of false -- rather, it’s a computation which when run, if it terminates, then it produces a proof of False. Of course, it can’t terminate. Ynot IO: Attempt #1:  Ynot IO: Attempt #1 IO : Set -andgt; Set return: forall (A:Set), A -andgt; IO A bind : forall (A B:Set), IO A -andgt; (A -andgt; IO B) -andgt; IO B ffix : forall (A:Set), (IO A -andgt; IO A) -andgt; IO A Reasoning about IO:  Reasoning about IO steps : IO A -andgt; IO A -andgt; Prop. steps_ret_bnd : forall (A B:Set)(v:A)(f:A-andgt;IO B), steps (bind (ret v) f) (f v). steps_bnd_cong : forall (A B:Set)(c1:IO A)(f:A-andgt;IO B), (steps c1 c2) -andgt; (steps (bind c1 f) (bind c2 f)). steps_ffix : forall (A:Set)(f:IO A-andgt;IO A), steps (ffix f) (f (ffix f)) Problem::  Problem: We have added a way to prove False! Sketch of problem (not quite right): Define diverges(c:IO A):Prop Define stepsn c1 c2 n as c1 steps to c2 in no more than n steps. Define diverges c as there’s no n and v such that stepsn c (ret v) n. Define T := { f : nat -andgt; IO nat | for some n, diverges(f n) } Problem Continued:  Problem Continued Next, define: f(p:T):T = {g;q } where g n = if n = 0 then 0 else (fst p)(n-1) and q argues that for some n, g diverges: (snd p) provides a proof that for some m, (fst p) diverges, so pick n=m+1. Finally, take F := ffix(f) snd(F) proves fst(F) diverges but fst(F) does not! How to Fix?:  How to Fix? One option: restrict IO to admissible types. In essence, we need closure conditions to ensure that fixed-points preserve typing. Comprehensions (subsets of types) are problematic in general. Crary shows some sufficient syntactic criteria for determining admissibility. Another option: don’t expose steps or any other axiom on IO terms. Well, we can expose some (the monad laws.) No Axioms?:  No Axioms? Can interpret IO A := unit. ret v = tt, bind v f = tt, ffix f = tt Without any axioms, can’t tell the difference! Allows us to establish consistency of logic. a trivial model. Aleks is then able to prove preservation and progress for the real operational semantics. But we have limited reasoning about computations within the system. Extending IO:  Extending IO We want to handle the awkward squad: Refs, IO, exceptions, concurrency, … So need to scale IO A. Today: refs, exceptions Tomorrow: IO Quite a ways off: concurrency? Heaps & Refs in Ynot:  Heaps andamp; Refs in Ynot We model heaps in Coq as follows: loc : Set loc_eq:(x y:loc)-andgt;{x=y}+{xandlt;andgt;y} can model locs as nats. dynamic := {T:Set; x:T} heap := loc -andgt; option dynamic NB: heaps aren’t 'Set' w/out impredicative IO Monad:  IO Monad Pre := heap -andgt; Prop Post(A:Set) := A -andgt; heap -andgt; heap -andgt; Prop IO: forall (A:Set), Pre -andgt; Post A -andgt; Post exn -andgt; Set. Implicit Arguments IO [A]. Return & Throw:  Return andamp; Throw ret : forall (A:Set)(x:A), IO (fun h =andgt; True) (fun y old h =andgt; y=x /\ h=old) (fun e old h =andgt; False) Implicit Arguments ret[A]. throw : forall (A:Set)(x:exn), IO (fun h =andgt; True) (fun y old h =andgt; False) (fun e old h =andgt; e=x /\ h=old) Reading a Location:  Reading a Location read : forall (A:Set)(x:loc), IO (fun h =andgt; exists v:A,mapsto h x v) (fun y old h =andgt; old = h /\ mapsto h x v) (fun e old h =andgt; False) where mapsto(A:Set)(h:heap)(x:loc)(v:A) := (h x) = Some(mkDynamic {A;v}} Writing a Location:  Writing a Location write : forall (A:Set)(x:loc)(v:A), IO (fun h =andgt; exists B, exists w:B, mapsto h x w) (fun y old h =andgt; y = tt /\ h = update old x A v) (fun e old h =andgt; False) Implicit Arguments write[A]. where update(h:heap)(x:loc)(A:Set)(v:A):heap := fun y =andgt; if (eq_loc x y) then Some(Dynamic{A,v}) else h y Bind:  Bind bind : forall (A B:Set)(P1:Pre)(Q1:Post A)(E1:Post exn) (P2:A-andgt;Pre)(Q2:A-andgt;Post B)(E2:A-andgt;Post exn), (IO A P1 Q1 E1) -andgt; (A -andgt; IO B P2 Q2 E2) -andgt; IO B (fun h =andgt; P1 h /\ (forall x m,(Q1 x h m) -andgt; P2 m)) (fun y old m =andgt; exists x m, (Q1 x old m) /\ (Q2 y m h)) (fun e old m =andgt; (E1 e old m) \/ (exists x m, (Q1 x old m) /\ (E2 e m h))) Implicit Arguments bind [A B P1 Q1 E1 P2 Q2 E2]. Using Bind:  Using Bind Definition readThen := fun (A B:Set)(x:loc) (p:A-andgt;pre)(q:A-andgt;post B) (e:A-andgt;post exn) (c:forall y:A, IO (p y) (q y) (e y))=andgt; bind (read A x) c. Implicit Arguments readThen [A B p q e]. Example::  Example: Definition swap := fun (A B:Set)(x y:loc) =andgt; (readThen x (fun (xv:A) =andgt; readThen y (fun (yv:B) =andgt; writeThen x yv (writeThen y xv (ret tt))))). Type Inferred for Swap:  Type Inferred for Swap forall (A B : Set) (x y : loc 1), IO (fun i : heap =andgt; (fun i0 : heap =andgt; exists v : A, mapsto i0 x v) i /\ (forall (x0 : A) (m : heap), (fun (y0 : A) (i0 m0 : heap) =andgt; mapsto i0 x y0 /\ m0 = i0) x0 i m -andgt; (fun (xv : A) (i0 : heap) =andgt; (fun i1 : heap =andgt; exists v : B, mapsto i1 y v) i0 /\ (forall (x1 : B) (m0 : heap), (fun (y0 : B) (i1 m1 : heap) =andgt; mapsto i1 y y0 /\ m1 = i1) x1 i0 m0 -andgt; (fun (yv : B) (i1 : heap) =andgt; (fun i2 : heap =andgt; exists B0 : Set, exists z : vector B0 1, mapsto_vec i2 x z) i1 /\ (forall (x2 : unit) (m1 : heap), (fun (_ : unit) (i2 m2 : heap) =andgt; m2 = update i2 x yv) x2 i1 m1 -andgt; (fun (_ : unit) (i2 : heap) =andgt; (fun i3 : heap =andgt; exists B0 : Set, exists z : vector B0 1, mapsto_vec i3 y z) i2 /\ (forall (x3 : unit) (m2 : heap), (fun (_ : unit) (i3 m3 : heap) =andgt; m3 = update i3 y xv) x3 i2 m2 -andgt; (fun _ : unit =andgt; nopre) x3 m2)) x2 m1)) x1 m0)) x0 m)) pre-condition only! Do:  Do do : forall (A:Set)(P1:Pre)(Q1:Post A)(E1:Post exn) (P2:Pre)(Q2:Post A)(E2:Post exn), (IO A P1 Q1 E1) -andgt; (forall h,(P2 h) -andgt; (P1 h)) -andgt; (forall y old m, (p2 old) -andgt; (Q1 y old m) -andgt; (Q2 y old m)) -andgt; (forall e old m, (p2 old) -andgt; (E1 y old m) -andgt; (E2 y old m)) -andgt; IO A P2 Q2 E2. Implicit Arguments do [A P1 Q1 E1]. Essentially, the rule of consequence. Ascribing a Spec to Swap:  Ascribing a Spec to Swap Program Definition swap_precise : forall (A B:Set)(x y:loc 1), IO (fun i =andgt; exists vx:A, exists vy:B, mapsto i x vx /\ mapsto i y vy) (fun (_:unit) i m =andgt; exists vx:A, exists vy:B, m = update (update i x vy) y vx) (fun _ _ _ =andgt; False) := fun A B x y =andgt; do (swap A B x y) _. Followed by a long proof. (can be shortened with combination of key lemmas and tactics.) Another Example::  Another Example: Definition InvIO(A:Set)(I:Pre) := IO I (fun (_:A) _ m =andgt; I m) (fun (_:exn) _ m =andgt; I m). Program Fixpoint mapIO(A B:Set)(I:pre) (f:A -andgt; B -andgt; InvIO B I (acc:B)(x:list A) {struct x} : InvIO B I := match x with | nil =andgt; do (ret acc) _ | cons h t =andgt; do (bind (f h acc) and#x4;and#x4; (fun acc2 =andgt; mapIO A B p q e pf f acc2 t)) _ end. Advantages:  Advantages For pure code: Can use refinements a la DML/ATS Or, can reason after the fact E.g., can prove append associative without having to tie it into the definition. Modeling language is serious e.g., heaps are defined in the model. Abstraction over values, types, specifications, and proofs (i.e., compositional!) If you stick to simple types, no proofs. Key Open Issues:  Key Open Issues Proofs are still painful. Need to adapt automation from ESC Need analogues to object invariants, ownership, etc. for mutable ADTs. Separation logic seems promising (next time). IO and other effects Need pre/post over worlds (heaps are just a part.) Better models? Predicate transformers seem promising Rasmus andamp; Lars working on denotational model

Related presentations


Other presentations created by Sabatini

energy Drink Presentation
26. 06. 2007
0 views

energy Drink Presentation

NatureV s Nurture
13. 09. 2007
0 views

NatureV s Nurture

Sponsorship
13. 09. 2007
0 views

Sponsorship

handout 185515
13. 09. 2007
0 views

handout 185515

R Piro
13. 09. 2007
0 views

R Piro

IDS presentation may02
13. 09. 2007
0 views

IDS presentation may02

WelcomeTo GUSD Special Education
03. 10. 2007
0 views

WelcomeTo GUSD Special Education

FEMA BCA Tornado
05. 10. 2007
0 views

FEMA BCA Tornado

Reference list sensors 10 2002
11. 09. 2007
0 views

Reference list sensors 10 2002

greek yogurt with honey
13. 09. 2007
0 views

greek yogurt with honey

honey traceability
13. 09. 2007
0 views

honey traceability

ppoint59
07. 10. 2007
0 views

ppoint59

The Persian Empire
11. 12. 2007
0 views

The Persian Empire

fitp 06
02. 11. 2007
0 views

fitp 06

seal
07. 11. 2007
0 views

seal

Teotihuacan
21. 11. 2007
0 views

Teotihuacan

Ph237Lecture1b
20. 11. 2007
0 views

Ph237Lecture1b

W4 Williams
07. 12. 2007
0 views

W4 Williams

cee500 fall01 solar
16. 11. 2007
0 views

cee500 fall01 solar

Apresentacao EEG Kappa rogerio
28. 12. 2007
0 views

Apresentacao EEG Kappa rogerio

history of computers
05. 01. 2008
0 views

history of computers

amanda
13. 09. 2007
0 views

amanda

1diary
02. 01. 2008
0 views

1diary

disaster recovery bof
28. 09. 2007
0 views

disaster recovery bof

gdc1999
13. 09. 2007
0 views

gdc1999

Andre bindevevssykdommer imm
04. 01. 2008
0 views

Andre bindevevssykdommer imm

Culturally Sensitive Approaches
24. 02. 2008
0 views

Culturally Sensitive Approaches

Dealer Training on DealerWorld
26. 02. 2008
0 views

Dealer Training on DealerWorld

Aravindan Ravi Bharath Kaka
28. 02. 2008
0 views

Aravindan Ravi Bharath Kaka

Hess INL
04. 10. 2007
0 views

Hess INL

f5c
26. 06. 2007
0 views

f5c

Egan BDNF val66met
26. 06. 2007
0 views

Egan BDNF val66met

dvd rental forecast
26. 06. 2007
0 views

dvd rental forecast

dlf 20061
26. 06. 2007
0 views

dlf 20061

Discover alive
26. 06. 2007
0 views

Discover alive

Depression center Apr 05
26. 06. 2007
0 views

Depression center Apr 05

IndiaChinaStudentVer sion
26. 03. 2008
0 views

IndiaChinaStudentVer sion

DMA Enviroment Webinar
27. 11. 2007
0 views

DMA Enviroment Webinar

ChristyJR SoComp 0710
07. 04. 2008
0 views

ChristyJR SoComp 0710

file 3
24. 11. 2007
0 views

file 3

Peter Leung
30. 03. 2008
0 views

Peter Leung

Filipino American Elders
01. 10. 2007
0 views

Filipino American Elders

busactivity
09. 04. 2008
0 views

busactivity

WEBVersionCN12808 12708FINAL
10. 04. 2008
0 views

WEBVersionCN12808 12708FINAL

mapbdtv2003
13. 04. 2008
0 views

mapbdtv2003

QuarterlyPres30Jun03
17. 04. 2008
0 views

QuarterlyPres30Jun03

WestCoast05Jun02
22. 04. 2008
0 views

WestCoast05Jun02

AH2
13. 09. 2007
0 views

AH2

wondersofhoney
13. 09. 2007
0 views

wondersofhoney

Future Czech Workforce RM
18. 03. 2008
0 views

Future Czech Workforce RM

GarmanSS2005
13. 03. 2008
0 views

GarmanSS2005

READING  NONFICTION  4
17. 06. 2007
0 views

READING NONFICTION 4

professions
17. 06. 2007
0 views

professions

part1
17. 06. 2007
0 views

part1

Noch mehr Cartoons
17. 06. 2007
0 views

Noch mehr Cartoons

Newspaper
17. 06. 2007
0 views

Newspaper

zielinski Slide Show Final
17. 06. 2007
0 views

zielinski Slide Show Final

touristen
17. 06. 2007
0 views

touristen

sites
17. 06. 2007
0 views

sites

simon 0600 isabel
17. 06. 2007
0 views

simon 0600 isabel

seks cartoons
17. 06. 2007
0 views

seks cartoons

What Every Employee Must Be Told
17. 06. 2007
0 views

What Every Employee Must Be Told

Violence
17. 06. 2007
0 views

Violence

Energy Film Festival
26. 06. 2007
0 views

Energy Film Festival

wolverhampton presentation
17. 06. 2007
0 views

wolverhampton presentation

fusionworkshop
11. 09. 2007
0 views

fusionworkshop

Ernte
12. 10. 2007
0 views

Ernte

ed price vide 2003
26. 06. 2007
0 views

ed price vide 2003

Media marktin Polen
17. 06. 2007
0 views

Media marktin Polen

riley1
17. 06. 2007
0 views

riley1

The Wacky Web and Other Goodies
17. 06. 2007
0 views

The Wacky Web and Other Goodies

p eilert codes standards cali
13. 09. 2007
0 views

p eilert codes standards cali

homelife
24. 02. 2008
0 views

homelife

oksupercompsymp2006 talk tummala
30. 12. 2007
0 views

oksupercompsymp2006 talk tummala

deca presentation
26. 06. 2007
0 views

deca presentation