-
- Downloads
Refactor modules; work on adequacy for intensional semantics
Showing
- formalizations/guarded-cubical/Common/Common.agda 19 additions, 0 deletionsformalizations/guarded-cubical/Common/Common.agda
- formalizations/guarded-cubical/Common/Later.agda 40 additions, 9 deletionsformalizations/guarded-cubical/Common/Later.agda
- formalizations/guarded-cubical/Common/Lemmas.agda 107 additions, 18 deletionsformalizations/guarded-cubical/Common/Lemmas.agda
- formalizations/guarded-cubical/Common/MonFuns.agda 88 additions, 34 deletionsformalizations/guarded-cubical/Common/MonFuns.agda
- formalizations/guarded-cubical/Interpretation.agda 0 additions, 91 deletionsformalizations/guarded-cubical/Interpretation.agda
- formalizations/guarded-cubical/Results.agda 0 additions, 251 deletionsformalizations/guarded-cubical/Results.agda
- formalizations/guarded-cubical/Results/Coinductive.agda 247 additions, 0 deletionsformalizations/guarded-cubical/Results/Coinductive.agda
- formalizations/guarded-cubical/Results/IntensionalAdequacy.agda 361 additions, 0 deletions...izations/guarded-cubical/Results/IntensionalAdequacy.agda
- formalizations/guarded-cubical/Semantics/Semantics.agda 246 additions, 114 deletionsformalizations/guarded-cubical/Semantics/Semantics.agda
- formalizations/guarded-cubical/Semantics/StrongBisimulation.agda 258 additions, 123 deletions...zations/guarded-cubical/Semantics/StrongBisimulation.agda
- formalizations/guarded-cubical/SyntacticTermPrecision.agda 0 additions, 170 deletionsformalizations/guarded-cubical/SyntacticTermPrecision.agda
- formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda 55 additions, 125 deletionsformalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
- formalizations/guarded-cubical/Syntax/GSTLC.agda 278 additions, 0 deletionsformalizations/guarded-cubical/Syntax/GSTLC.agda
- formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda 66 additions, 0 deletionsformalizations/guarded-cubical/Syntax/GSTLCCollapse.agda
Loading
Please register or sign in to comment