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.01Aug28Jul25201811325Jun2085432131May3029282725242322181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861add new file: PosetWithPtbAddition to monotone combinatorsUpdates to lock-step error ordering fileAdditions to Common.agdaUpdates to monotone relationsInit abstract modelNew formulation of Dyn as a PosetInit poset modeladditions to thin double catBegin formalizing thin double categoriesUpdates to monotone-related filesAdditions to Common.agdaBegin concrete poset semanticsMore poset stuffMonotone stuffDyn as a PosetLock step error orderingMore properties of laterExtensional Surfish Syntax and Intensional Terms/Logicprove clocked relation associativityRemove some code in IntensionalAdequacy.agdaInit LaterProperties.agdaUpdate Common.agdaUpdate Lift.agdaUpdate Global.agdafix not in scope errorUpdates to Lift fileupdate Later fileprove clocked relation identity rightRefactor preorder and monotone function codeError ordering on Delay function typeMove Delay-related files to SemanticsA relational view on our monad (incomplete)some writing[abstract semantics] error strictness, ret and ret βηmore progress on semantics: plugging ev ctxts and their equationsupdate to extensionsystem version of comonads/strong monadsprove substId/substAssoc for EvCtxev ctxts all done except for substId/substAssoc and the computation stuffBegin formalizing coalgebras categorically