Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • main default protected
  • master
2 results
Created with Raphaël 2.2.031Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861delete some old commentsembiggen the discussion sectionembiggen the decomplexification and logical relation sectionsembiggen the gtt to cbpv sectionfix some space stuff, use overlines in the cast lemmasMerge branch 'master' of github.ccs.neu.edu:coqatoos/cbv-gradual-type-theoryintro editsthe cbv to gtt sectionfinish updates on sec 3 (biggest changes)Merge branch 'master' of github.ccs.neu.edu:coqatoos/cbv-gradual-type-theoryintro editsmove stuff around, finish least dyn subsectionMerge branch 'master' of github.ccs.neu.edu:coqatoos/cbv-gradual-type-theoryintro editscheckinexpanding figuresfix bibliography issuesvery littlefinish the cbv to gtt proofsmore proofs, including function cast reduction stepcbv syntax, op semantics, translationadd jfp bibmigrate to jfp-paper/jfp-gtt.texRevert "start adding recursive value types"include defs!some more cbv gttsome translationcbv function uniqueness proofpenn talk updateinit jfpadd penn talkwrite up my gradual type theory talk notestalk doneexamplesoutline of talk on mondaystart adding recursive value typesshow how recursive types work as least pre-fixed pointssome notes on extending GTT with recursive typesfinal version of talkprobably final slides