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.023May22181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861WIP on explicit substitution (much simpler so far)Some syntax experimentswork on new syntxBegin porting syntax to GTT and new Context repnew syntax in progressDefine preorder-enriched cats, refl. graph of preorder enriched catsMerge branch 'main' of https://gitlab.eecs.umich.edu/gradual-typing/sgdtchanges to wordingwork on paper (changes to intro, work on description of syntax)syntax discussed in today's meetingcheck in technical notes documentsketch of categorical semanticsMore work on paperRemove old fileMore code refactoring/cleanupRefactor modules; work on adequacy for intensional semanticsupdate gitignorecheck-in reading group presentationwork on paperChanges to Later.agda: add dependent force function (where the type can mention the clock); remove "global" clock-irrel axiom, instead axiomatize it on a per-type basisUpdate gitignoreWork on intensional and extensional theoriesnotes on lift monad in topos of trees modelinit new paperMerge branch 'main' of https://gitlab.eecs.umich.edu/gradual-typing/sgdtpredomains as posets; monotone function combinatorsMore guarded cat ideastheta as a left adjoint?A simpler definition of Dyn?denotational semanticsweaken the assumption to apply to the weak bisimulation relfix merge issuefix merge issueMerge branch 'main' of https://gitlab.eecs.umich.edu/gradual-typing/sgdtmergecompletely eliminate the need for symmetry in the proofshow symmetry can be replaced by reflexivity (at fix \theta)syntactic properties of type precisiondefine infix mapSyntax of gradual CBV cast calculus