minidot/dev2015 at master · TiarkRompf/minidot

History

Name		Name	Last commit message	Last commit date
parent directory ..
README.md		README.md
SfLib.v		SfLib.v
dot-smallstep1.v		dot-smallstep1.v
dot-smallstep2.v		dot-smallstep2.v
dot-smallstep3.v		dot-smallstep3.v
dot-smallstep3a.v		dot-smallstep3a.v
dot-smallstep3b.v		dot-smallstep3b.v
dot-smallstep3c.v		dot-smallstep3c.v
dot-smallstep4.v		dot-smallstep4.v
dot-smallstep5.v		dot-smallstep5.v
dot-smallstep6.v		dot-smallstep6.v
dot-stp-single1.v		dot-stp-single1.v
dot-stp-single2.v		dot-stp-single2.v
dot-stp-single3.v		dot-stp-single3.v
dot10.v		dot10.v
dot11-wip.v		dot11-wip.v
dot12.v		dot12.v
dot13.v		dot13.v
dot14.v		dot14.v
dot15.v		dot15.v
dot16.v		dot16.v
dot17.v		dot17.v
dot18.v		dot18.v
dot19.v		dot19.v
dot2.v		dot2.v
dot20.v		dot20.v
dot21.v		dot21.v
dot22.v		dot22.v
dot23.v		dot23.v
dot24.v		dot24.v
dot25-wip.v		dot25-wip.v
dot26.v		dot26.v
dot27.v		dot27.v
dot28.v		dot28.v
dot29.v		dot29.v
dot3.v		dot3.v
dot30-wip.v		dot30-wip.v
dotb.v		dotb.v
fsub0.v		fsub0.v
fsub1.v		fsub1.v
fsub2.v		fsub2.v
fsub3.v		fsub3.v
fsub4-strong.v		fsub4-strong.v
fsub4.v		fsub4.v
fsub5.v		fsub5.v
nano0.v		nano0.v
nano1.v		nano1.v
nano2.v		nano2.v
nano3.v		nano3.v
nano4-1-smallstep.v		nano4-1-smallstep.v
nano4-1-smallstep0.v		nano4-1-smallstep0.v
nano4-1.v		nano4-1.v
nano4-2.v		nano4-2.v
nano4-3.v		nano4-3.v
nano4-4.v		nano4-4.v
nano4-5.v		nano4-5.v
nano4-6.v		nano4-6.v
nano4-7.v		nano4-7.v
nano4-8.v		nano4-8.v
nano4.v		nano4.v
singletons.v		singletons.v
singletons1.v		singletons1.v
singletons2.v		singletons2.v
sms-singletons0-latest-wip.v		sms-singletons0-latest-wip.v
sms-singletons0.v		sms-singletons0.v
sms-singletons1-wip.v		sms-singletons1-wip.v
sms-singletons2-wip.v		sms-singletons2-wip.v
stp-singletons0.v		stp-singletons0.v
stp-singletons1.v		stp-singletons1.v

README.md

From F to DOT: Type Soundness Proofs with Definitional Interpreters [pdf]
- big-step
  - simply typed lambda calculus
  - F_<:
  - D_<:> (F_<: with first-class types and lower bounds)
  - D_<:> with state (add mutable references to D_<:)
  - full DOT (D_<:> plus intersection and union types, recursive self types, compound objects, ...)
- back to small-step
  - sketch
  - full DOT

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

dev2015

dev2015

README.md

Files

dev2015

Directory actions

More options

Directory actions

More options

Latest commit

History

dev2015

Folders and files

parent directory

README.md