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.020Jul1811325Jun2085432131May3029282725242322181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861additions 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 categoricallyProof that Delay is a final coalgebraDelay datatypeMove global lift code into separate filemore progress on evaluation contexts, stuck on an upstream issuemost of value semantics, start EvCtx semanticsWIP on term semantics: substitutions and some of valuesmodel of types and precision in an abstract modelmake isProp⊑ admissible