Index of /~nad/listings/up-to

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.Builtin.Bool.html 12-Jul-2018 14:23 2.4K 
[TXT]Agda.Builtin.Equalit..>12-Jul-2018 14:23 2.3K 
[TXT]Agda.Builtin.List.html 12-Jul-2018 14:23 3.6K 
[TXT]Agda.Builtin.Nat.html 12-Jul-2018 14:23 18K 
[TXT]Agda.Builtin.Size.html 12-Jul-2018 14:23 2.9K 
[TXT]Agda.Builtin.Unit.html 12-Jul-2018 14:23 1.2K 
[TXT]Agda.Primitive.html 12-Jul-2018 14:23 3.6K 
[TXT]Agda.css 12-Jul-2018 14:23 1.2K 
[TXT]Bijection.html 12-Jul-2018 14:23 157K 
[TXT]Bisimilarity.6-2-5.html12-Jul-2018 14:23 94K 
[TXT]Bisimilarity.html 12-Jul-2018 14:23 54K 
[TXT]Bisimilarity.CCS.Cla..>12-Jul-2018 14:23 95K 
[TXT]Bisimilarity.CCS.html 12-Jul-2018 14:23 365K 
[TXT]Bisimilarity.CCS.Exa..>12-Jul-2018 14:23 61K 
[TXT]Bisimilarity.CCS.Exa..>12-Jul-2018 14:23 62K 
[TXT]Bisimilarity.CCS.Exa..>12-Jul-2018 14:23 479K 
[TXT]Bisimilarity.CCS.Gen..>12-Jul-2018 14:23 85K 
[TXT]Bisimilarity.Classic..>12-Jul-2018 14:23 5.0K 
[TXT]Bisimilarity.Classic..>12-Jul-2018 14:23 131K 
[TXT]Bisimilarity.Compari..>12-Jul-2018 14:23 81K 
[TXT]Bisimilarity.Delay-m..>12-Jul-2018 14:23 21K 
[TXT]Bisimilarity.Equatio..>12-Jul-2018 14:23 19K 
[TXT]Bisimilarity.General..>12-Jul-2018 14:23 105K 
[TXT]Bisimilarity.Step.html 12-Jul-2018 14:23 68K 
[TXT]Bisimilarity.Up-to.C..>12-Jul-2018 14:23 114K 
[TXT]Bisimilarity.Up-to.html12-Jul-2018 14:23 21K 
[TXT]Bisimilarity.Up-to.C..>12-Jul-2018 14:23 305K 
[TXT]Bisimilarity.Weak.Al..>12-Jul-2018 14:23 4.4K 
[TXT]Bisimilarity.Weak.Al..>12-Jul-2018 14:23 46K 
[TXT]Bisimilarity.Weak.Al..>12-Jul-2018 14:23 14K 
[TXT]Bisimilarity.Weak.Al..>12-Jul-2018 14:23 29K 
[TXT]Bisimilarity.Weak.Al..>12-Jul-2018 14:23 19K 
[TXT]Bisimilarity.Weak.html 12-Jul-2018 14:23 91K 
[TXT]Bisimilarity.Weak.CC..>12-Jul-2018 14:23 292K 
[TXT]Bisimilarity.Weak.CC..>12-Jul-2018 14:23 200K 
[TXT]Bisimilarity.Weak.De..>12-Jul-2018 14:23 156K 
[TXT]Bisimilarity.Weak.Eq..>12-Jul-2018 14:23 85K 
[TXT]Bisimilarity.Weak.Eq..>12-Jul-2018 14:23 23K 
[TXT]Bisimilarity.Weak.Up..>12-Jul-2018 14:23 95K 
[TXT]Bisimilarity.Weak.Up..>12-Jul-2018 14:23 66K 
[TXT]Bool.html 12-Jul-2018 14:23 66K 
[TXT]Delay-monad.Bisimila..>12-Jul-2018 14:23 57K 
[TXT]Delay-monad.Bisimila..>12-Jul-2018 14:23 9.0K 
[TXT]Delay-monad.Bisimila..>12-Jul-2018 14:23 208K 
[TXT]Delay-monad.html 12-Jul-2018 14:23 14K 
[TXT]Delay-monad.Bisimila..>12-Jul-2018 14:23 193K 
[TXT]Delay-monad.Partial-..>12-Jul-2018 14:23 156K 
[TXT]Delay-monad.Terminat..>12-Jul-2018 14:23 42K 
[TXT]Double-negation.html 12-Jul-2018 14:23 40K 
[TXT]Embedding.html 12-Jul-2018 14:23 62K 
[TXT]Equality.Decidable-U..>12-Jul-2018 14:23 70K 
[TXT]Equality.Decision-pr..>12-Jul-2018 14:23 80K 
[TXT]Equality.Groupoid.html 12-Jul-2018 14:23 104K 
[TXT]Equality.Proposition..>12-Jul-2018 14:23 13K 
[TXT]Equality.Tactic.html 12-Jul-2018 14:23 143K 
[TXT]Equality.html 12-Jul-2018 14:23 827K 
[TXT]Equational-reasoning..>12-Jul-2018 14:23 65K 
[TXT]Equivalence.html 12-Jul-2018 14:23 652K 
[TXT]Expansion.CCS.html 12-Jul-2018 14:23 340K 
[TXT]Expansion.html 12-Jul-2018 14:23 102K 
[TXT]Expansion.Delay-mona..>12-Jul-2018 14:23 85K 
[TXT]Expansion.Equational..>12-Jul-2018 14:23 44K 
[TXT]Fin.html 12-Jul-2018 14:23 179K 
[TXT]Function-universe.html 12-Jul-2018 14:23 1.4M 
[TXT]Groupoid.html 12-Jul-2018 14:23 46K 
[TXT]H-level.Closure.html 12-Jul-2018 14:23 298K 
[TXT]H-level.html 12-Jul-2018 14:23 39K 
[TXT]Indexed-container.html 12-Jul-2018 14:23 262K 
[TXT]Indexed-container.Co..>12-Jul-2018 14:23 588K 
[TXT]Indexed-container.De..>12-Jul-2018 14:23 61K 
[TXT]Injection.html 12-Jul-2018 14:23 17K 
[TXT]Labelled-transition-..>12-Jul-2018 14:23 16K 
[TXT]Labelled-transition-..>12-Jul-2018 14:23 235K 
[TXT]Labelled-transition-..>12-Jul-2018 14:23 351K 
[TXT]Labelled-transition-..>12-Jul-2018 14:23 119K 
[TXT]Labelled-transition-..>12-Jul-2018 14:23 104K 
[TXT]List.html 12-Jul-2018 14:23 78K 
[TXT]Logical-equivalence...>12-Jul-2018 14:23 20K 
[TXT]Monad.html 12-Jul-2018 14:23 126K 
[TXT]Nat.html 12-Jul-2018 14:23 257K 
[TXT]Preimage.html 12-Jul-2018 14:23 59K 
[TXT]Prelude.html 12-Jul-2018 14:23 125K 
[TXT]README.html 12-Jul-2018 14:23 16K 
[TXT]README.Pointers-to-r..>12-Jul-2018 14:23 84K 
[TXT]Relation.html 12-Jul-2018 14:23 215K 
[TXT]Similarity.CCS.html 12-Jul-2018 14:23 133K 
[TXT]Similarity.Equationa..>12-Jul-2018 14:23 25K 
[TXT]Similarity.General.html12-Jul-2018 14:23 45K 
[TXT]Similarity.html 12-Jul-2018 14:23 28K 
[TXT]Similarity.Step.html 12-Jul-2018 14:23 330K 
[TXT]Similarity.Weak.Equa..>12-Jul-2018 14:23 48K 
[TXT]Similarity.Weak.Up-t..>12-Jul-2018 14:23 9.9K 
[TXT]Similarity.Weak.html 12-Jul-2018 14:23 49K 
[TXT]Surjection.html 12-Jul-2018 14:23 51K 
[TXT]Univalence-axiom.html 12-Jul-2018 14:23 567K 
[TXT]Up-to.Closure.html 12-Jul-2018 14:23 109K 
[TXT]Up-to.Via.html 12-Jul-2018 14:23 83K 
[TXT]Up-to.html 12-Jul-2018 14:23 283K 

README
------------------------------------------------------------------------
-- Code related to the paper "Up-to Techniques using Sized Types"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module README where

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Some preliminaries

-- Overloaded "equational" reasoning combinators.

import Equational-reasoning

-- Unary and binary relations.

import Relation

------------------------------------------------------------------------
-- Containers

-- Indexed containers.

import Indexed-container

-- Container combinators.

import Indexed-container.Combinators

-- The delay monad defined as the greatest fixpoint of an indexed
-- container.

import Indexed-container.Delay-monad

------------------------------------------------------------------------
-- Up-to techniques

-- Up-to techniques, compatibility, size-preserving functions, and the
-- companion.

import Up-to

-- Closure properties for Compatible and Size-preserving.
--
-- (Some negative results in this module depend on code presented
-- further down.)

import Up-to.Closure

-- Up-to techniques via.

import Up-to.Via

------------------------------------------------------------------------
-- Labelled transition systems

-- Labelled transition systems (LTSs).

import Labelled-transition-system
import Labelled-transition-system.Equational-reasoning-instances

-- CCS.

import Labelled-transition-system.CCS

-- A labelled transition system for the delay monad.

import Labelled-transition-system.Delay-monad

-- An LTS from Section 6.2.5 of "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi.

import Labelled-transition-system.6-2-5

------------------------------------------------------------------------
-- Similarity

-- The one-sided Step function, used to define similarity and the
-- two-sided Step function.

import Similarity.Step

-- A parametrised coinductive definition that can be used to define
-- various forms of similarity.

import Similarity.General

-- For more information about similarity, see "Similarity, continued"
-- below.

------------------------------------------------------------------------
-- Strong bisimilarity

-- The Step function, used to define strong and weak bisimilarity as
-- well as expansion.

import Bisimilarity.Step

-- A parametrised coinductive definition that can be used to define
-- strong and weak bisimilarity as well as expansion.

import Bisimilarity.General

-- A coinductive definition of (strong) bisimilarity.

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances

-- The classical definition of (strong) bisimilarity.

import Bisimilarity.Classical
import Bisimilarity.Classical.Equational-reasoning-instances

-- A comparison of the two definitions of bisimilarity.

import Bisimilarity.Comparison

-- Some results related to strong bisimilarity for the delay monad.

import Bisimilarity.Delay-monad

-- Some results related to CCS, implemented without using a fixed form
-- of bisimilarity.

import Bisimilarity.CCS.General

-- Various results or examples related to CCS, implemented using the
-- coinductive definition of bisimilarity.

import Bisimilarity.CCS
import Bisimilarity.CCS.Examples
import Bisimilarity.CCS.Examples.Natural-numbers

-- Some of the results/examples above have also been implemented using
-- the classical definition of bisimilarity.

import Bisimilarity.CCS.Classical
import Bisimilarity.CCS.Examples.Classical

-- Up-to techniques for strong bisimilarity.

import Bisimilarity.Up-to
import Bisimilarity.Up-to.CCS
import Bisimilarity.Up-to.Counterexamples

-- Some results related to an LTS from Section 6.2.5 of "Enhancements
-- of the bisimulation proof method" by Pous and Sangiorgi,
-- implemented using the coinductive definition of bisimilarity.

import Bisimilarity.6-2-5

------------------------------------------------------------------------
-- Expansion

-- A coinductive definition of the expansion ordering.

import Expansion
import Expansion.Equational-reasoning-instances

-- Lemmas related to expansion and CCS.

import Expansion.CCS

-- Some results related to expansion for the delay monad.

import Expansion.Delay-monad

------------------------------------------------------------------------
-- Weak bisimilarity

-- A coinductive definition of weak bisimilarity.

import Bisimilarity.Weak
import Bisimilarity.Weak.Equational-reasoning-instances

-- An alternative (non-standard) coinductive definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances

-- An alternative (non-standard) classical definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative.Classical

-- A comparison of the two alternative definitions of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative.Comparison

-- The two coinductive definitions of weak bisimilarity are pointwise
-- logically equivalent.

import Bisimilarity.Weak.Equivalent

-- Lemmas related to weak bisimilarity and CCS.

import Bisimilarity.Weak.CCS

-- Examples/exercises related to CCS from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

import Bisimilarity.Weak.CCS.Examples

-- Some results about various forms of coinductively defined weak
-- bisimilarity for the delay monad.

import Bisimilarity.Weak.Delay-monad

-- Up-to techniques for the standard coinductive definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Up-to
import Bisimilarity.Weak.Up-to.CCS

-- Up-to techniques for the delay monad and the alternative
-- coinductive definition of weak bisimilarity.

import Bisimilarity.Weak.Alternative.Up-to.Delay-monad

------------------------------------------------------------------------
-- Similarity, continued

-- A coinductive definition of (strong) similarity.

import Similarity
import Similarity.Equational-reasoning-instances

-- Lemmas related to strong similarity for CCS.

import Similarity.CCS

-- A coinductive definition of weak similarity.

import Similarity.Weak
import Similarity.Weak.Equational-reasoning-instances

-- An up-to technique for weak similarity.

import Similarity.Weak.Up-to