Index of /~nad/listings/up-to

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Up-to.html 04-Dec-2017 12:21 299K 
[TXT]Up-to.Via.html 04-Dec-2017 12:21 89K 
[TXT]Up-to.Closure.html 04-Dec-2017 12:21 113K 
[TXT]Univalence-axiom.html 04-Dec-2017 12:21 589K 
[TXT]Surjection.html 04-Dec-2017 12:21 51K 
[TXT]Similarity.html 04-Dec-2017 12:21 30K 
[TXT]Similarity.Weak.html 04-Dec-2017 12:21 52K 
[TXT]Similarity.Weak.Up-t..>04-Dec-2017 12:21 10K 
[TXT]Similarity.Weak.Equa..>04-Dec-2017 12:21 50K 
[TXT]Similarity.Step.html 04-Dec-2017 12:21 343K 
[TXT]Similarity.General.html04-Dec-2017 12:21 47K 
[TXT]Similarity.Equationa..>04-Dec-2017 12:21 25K 
[TXT]Similarity.CCS.html 04-Dec-2017 12:21 136K 
[TXT]Relation.html 04-Dec-2017 12:21 219K 
[TXT]README.html 04-Dec-2017 12:21 16K 
[TXT]README.Pointers-to-r..>04-Dec-2017 12:21 86K 
[TXT]Prelude.html 04-Dec-2017 12:21 127K 
[TXT]Preimage.html 04-Dec-2017 12:21 60K 
[TXT]Nat.html 04-Dec-2017 12:21 88K 
[TXT]Monad.html 04-Dec-2017 12:21 127K 
[TXT]Logical-equivalence...>04-Dec-2017 12:21 20K 
[TXT]List.html 04-Dec-2017 12:21 61K 
[TXT]Labelled-transition-..>04-Dec-2017 12:21 247K 
[TXT]Labelled-transition-..>04-Dec-2017 12:21 108K 
[TXT]Labelled-transition-..>04-Dec-2017 12:21 124K 
[TXT]Labelled-transition-..>04-Dec-2017 12:21 365K 
[TXT]Labelled-transition-..>04-Dec-2017 12:21 16K 
[TXT]Injection.html 04-Dec-2017 12:21 17K 
[TXT]Indexed-container.html 04-Dec-2017 12:21 271K 
[TXT]Indexed-container.De..>04-Dec-2017 12:21 64K 
[TXT]Indexed-container.Co..>04-Dec-2017 12:21 621K 
[TXT]H-level.html 04-Dec-2017 12:21 40K 
[TXT]H-level.Closure.html 04-Dec-2017 12:21 302K 
[TXT]Groupoid.html 04-Dec-2017 12:21 49K 
[TXT]Function-universe.html 04-Dec-2017 12:21 1.5M 
[TXT]Fin.html 04-Dec-2017 12:21 117K 
[TXT]Expansion.html 04-Dec-2017 12:21 108K 
[TXT]Expansion.Equational..>04-Dec-2017 12:21 45K 
[TXT]Expansion.Delay-mona..>04-Dec-2017 12:21 90K 
[TXT]Expansion.CCS.html 04-Dec-2017 12:21 347K 
[TXT]Equivalence.html 04-Dec-2017 12:21 666K 
[TXT]Equational-reasoning..>04-Dec-2017 12:21 68K 
[TXT]Equality.html 04-Dec-2017 12:21 859K 
[TXT]Equality.Tactic.html 04-Dec-2017 12:21 147K 
[TXT]Equality.Proposition..>04-Dec-2017 12:21 13K 
[TXT]Equality.Groupoid.html 04-Dec-2017 12:21 105K 
[TXT]Equality.Decision-pr..>04-Dec-2017 12:21 81K 
[TXT]Equality.Decidable-U..>04-Dec-2017 12:21 71K 
[TXT]Embedding.html 04-Dec-2017 12:21 64K 
[TXT]Double-negation.html 04-Dec-2017 12:21 39K 
[TXT]Delay-monad.html 04-Dec-2017 12:21 14K 
[TXT]Delay-monad.Weak-bis..>04-Dec-2017 12:21 337K 
[TXT]Delay-monad.Strong-b..>04-Dec-2017 12:21 45K 
[TXT]Delay-monad.Partial-..>04-Dec-2017 12:21 166K 
[TXT]Delay-monad.Expansio..>04-Dec-2017 12:21 215K 
[TXT]Bool.html 04-Dec-2017 12:21 69K 
[TXT]Bisimilarity.html 04-Dec-2017 12:21 58K 
[TXT]Bisimilarity.Weak.html 04-Dec-2017 12:21 98K 
[TXT]Bisimilarity.Weak.Up..>04-Dec-2017 12:21 98K 
[TXT]Bisimilarity.Weak.Up..>04-Dec-2017 12:21 67K 
[TXT]Bisimilarity.Weak.Eq..>04-Dec-2017 12:21 25K 
[TXT]Bisimilarity.Weak.Eq..>04-Dec-2017 12:21 88K 
[TXT]Bisimilarity.Weak.De..>04-Dec-2017 12:21 164K 
[TXT]Bisimilarity.Weak.CC..>04-Dec-2017 12:21 204K 
[TXT]Bisimilarity.Weak.CC..>04-Dec-2017 12:21 301K 
[TXT]Bisimilarity.Weak.Al..>04-Dec-2017 12:21 20K 
[TXT]Bisimilarity.Weak.Al..>04-Dec-2017 12:21 30K 
[TXT]Bisimilarity.Weak.Al..>04-Dec-2017 12:21 14K 
[TXT]Bisimilarity.Weak.Al..>04-Dec-2017 12:21 47K 
[TXT]Bisimilarity.Weak.Al..>04-Dec-2017 12:21 4.7K 
[TXT]Bisimilarity.Up-to.html04-Dec-2017 12:21 22K 
[TXT]Bisimilarity.Up-to.C..>04-Dec-2017 12:21 315K 
[TXT]Bisimilarity.Up-to.C..>04-Dec-2017 12:21 116K 
[TXT]Bisimilarity.Step.html 04-Dec-2017 12:21 72K 
[TXT]Bisimilarity.General..>04-Dec-2017 12:21 111K 
[TXT]Bisimilarity.Equatio..>04-Dec-2017 12:21 20K 
[TXT]Bisimilarity.Delay-m..>04-Dec-2017 12:21 21K 
[TXT]Bisimilarity.Compari..>04-Dec-2017 12:21 83K 
[TXT]Bisimilarity.Classic..>04-Dec-2017 12:21 137K 
[TXT]Bisimilarity.Classic..>04-Dec-2017 12:21 5.2K 
[TXT]Bisimilarity.CCS.html 04-Dec-2017 12:21 371K 
[TXT]Bisimilarity.CCS.Gen..>04-Dec-2017 12:21 87K 
[TXT]Bisimilarity.CCS.Exa..>04-Dec-2017 12:21 488K 
[TXT]Bisimilarity.CCS.Exa..>04-Dec-2017 12:21 64K 
[TXT]Bisimilarity.CCS.Exa..>04-Dec-2017 12:21 62K 
[TXT]Bisimilarity.CCS.Cla..>04-Dec-2017 12:21 96K 
[TXT]Bisimilarity.6-2-5.html04-Dec-2017 12:21 96K 
[TXT]Bijection.html 04-Dec-2017 12:21 161K 
[TXT]Agda.css 04-Dec-2017 12:21 1.2K 
[TXT]Agda.Primitive.html 04-Dec-2017 12:21 3.6K 
[TXT]Agda.Builtin.Unit.html 04-Dec-2017 12:21 1.2K 
[TXT]Agda.Builtin.Size.html 04-Dec-2017 12:21 1.7K 
[TXT]Agda.Builtin.Nat.html 04-Dec-2017 12:21 18K 
[TXT]Agda.Builtin.List.html 04-Dec-2017 12:21 4.3K 
[TXT]Agda.Builtin.Equalit..>04-Dec-2017 12:21 2.3K 
[TXT]Agda.Builtin.Bool.html 04-Dec-2017 12:21 2.5K 

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