Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • hl2
  • hl2_cat
  • master default
3 results
Created with Raphaël 2.2.026May258729Apr282423221110973213Mar27Nov2120188731Oct28262520181615141310330Aug29Jul2625231211987543226Jun25242322212019181714131211107630May2724232217161211109876543130Apr262423221932128Mar272522201918136549Feb87Jan26Dec251918171412865430Nov292126Oct2595328Sep27129529Aug191815111098732131Jul2130Jun29282726242322121198Add typeclass infrastructure for determining if Σ is compatible with a LogExts.hl2_cathl2_catBegin adding infrasturcture for constrainting `Σ`.Switch to `gFunctors`-esque list-based approached instead of categorical approach.This is where I give up on fighting universe issues.Setup category theory for `LogExt`.Set up category theory background for semantic extensions.Fix build.Prove needed inversion lemmata for `ReSumC`.Implement missing type-classes for `HomSynExt`.Prove that the resum solver actually builds an isomorphism (will be useful later).Add heap language extension.Add new resum solver which keeps track of identification with sum.Finish adding atomic blocks to HeapLang 2.0.Start adding atomic blocks to HeapLang 2.0.Add abstractions for doing atomic blocks.Begin implementing heap language extension.Port program logic, use typeclasses for fixing "global" semantic/syntactic extension.Fix bind lemma.Bail on previous two approaches: use an amalgamation between categorical and list-based approach.Begin to move away from categorical approach to "fixed universe" approach.hl2hl2Add partial implementation of extensible lambda calculus.Update Iris version.mastermastermention affiliation in copyrightfix some footnote referencesfix markdownmake more things linksmake readme link to paper websiteMerge branch 'master' of https://gitlab.mpi-sws.org/iris/itree-program-logicenable CI hereAdd Coq/paper mapping.remove leftover filesMerge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itreeUpdate ExampleLang formalization to paper.add licenseadd LICENSE to islarisMerge branch 'master' of gitlab.inf.ethz.ch:ou-plf/iris-itreeUse `solve_ndisj` one more place.bump dependencies and fix buildAdd `spinlock` to `_CoqProject`.Use `solve_ndisj` tactic instead of manual reasoning.