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.017Nov1614624Oct1913109875329Sep26222015730Aug2823221584128Jul25201811325Jun2085432131May3029282725242322181725Apr2014131Mar30292123Feb1312Jan411Dec20Oct181211417Aug27Jul21191824May218Jan74331Dec2416151488Sep31Jan3010876319Jun4Apr19Mar151423Feb131217Jan161121Nov96530Oct2928262524221121Sep2025Jul12111098767653230Jun292827262522212019181716151413121130May26252422211298654329Apr2726252420177643230Mar2861remove outdated pdfbegin description of denotational model for intensional gradual typingelimination form of intensional order (very slow)merge two cases(casenat/arr) into one casedyncheck in latex style filebegin rearranging: discuss term syn/sem and then ordering syn/semupdate cubical library pathmore fixes after updating cubical libraryupdates to Later.agdaupdate to agda 2.6.4 and cubical-0.6update definitions filecheck in semantics file before making changescheck in current syntax file before making changesUpdate translation from surface to intensionalUpdate SyntacticBisimilarityUpdate IntensionalOrderBegin new version of intensional term semantics using eliminatorElimination principle for intensional termsUpdate syntactic bisimilarityAdd DPMorProofsadd lift properties for extLAdd lemmas for representable relationadd Terms for DoublePoset SemanticsAdd DoublePoset files (corresponding to Poset)make up DPCombinatorsResults about intensional term syntaxIntensional term semanticsSyntactic bisimilarityIntensional orderingTranslation from surface to intensionalSurface syntax and logicrepresentableRelation on injNat, injArrsome work on normalizationone easy manual case of normalization proofsome progress on the monad simplifier proof. Used the Nbe solver forimplement the end-to-end monad normalization functionoutline of normalizationImplement Nbe for solving substitution equationswork on nbenbe stuff