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.020Jun85432131May3029282725242322181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861Update 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⊑ admissibleA convenient abstract semantics of the term languagea (full?) formulation of a term modelstart working on the abstract models. First the term languageCat of preorders; preorder-enriched cat of preordersPreorders and monotone functionsRefactoringsome example gtt theoremsImplement the GTT logic, reduce the amount of annotations using nested var generalizationlower the universe level of the termsfinish the term syntax, init the logicWIP on explicit substitution (much simpler so far)Some syntax experimentswork on new syntxBegin porting syntax to GTT and new Context rep