Index of /~nad/listings/up-to

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Up-to.html 06-Sep-2017 22:28 215K 
[TXT]Up-to.Via.html 06-Sep-2017 22:28 88K 
[TXT]Up-to.Closure.html 06-Sep-2017 22:28 100K 
[TXT]Univalence-axiom.html 06-Sep-2017 22:28 586K 
[TXT]Surjection.html 06-Sep-2017 22:28 51K 
[TXT]Similarity.Weak.html 06-Sep-2017 22:28 36K 
[TXT]Similarity.Weak.Up-t..>06-Sep-2017 22:28 10K 
[TXT]Similarity.Weak.Equa..>06-Sep-2017 22:28 51K 
[TXT]Similarity.Strong.html 06-Sep-2017 22:28 16K 
[TXT]Similarity.Strong.Eq..>06-Sep-2017 22:28 27K 
[TXT]Similarity.Strong.CC..>06-Sep-2017 22:28 139K 
[TXT]Similarity.Step.html 06-Sep-2017 22:28 337K 
[TXT]Similarity.General.html06-Sep-2017 22:28 48K 
[TXT]Relation.html 06-Sep-2017 22:28 203K 
[TXT]README.html 06-Sep-2017 22:28 15K 
[TXT]README.Pointers-to-r..>06-Sep-2017 22:28 59K 
[TXT]Prelude.html 06-Sep-2017 22:28 127K 
[TXT]Preimage.html 06-Sep-2017 22:28 60K 
[TXT]Nat.html 06-Sep-2017 22:28 88K 
[TXT]Monad.html 06-Sep-2017 22:28 126K 
[TXT]Logical-equivalence...>06-Sep-2017 22:28 20K 
[TXT]List.html 06-Sep-2017 22:28 61K 
[TXT]Labelled-transition-..>06-Sep-2017 22:28 239K 
[TXT]Labelled-transition-..>06-Sep-2017 22:28 107K 
[TXT]Labelled-transition-..>06-Sep-2017 22:28 122K 
[TXT]Labelled-transition-..>06-Sep-2017 22:28 234K 
[TXT]Labelled-transition-..>06-Sep-2017 22:28 17K 
[TXT]Interval.html 06-Sep-2017 22:28 73K 
[TXT]Injection.html 06-Sep-2017 22:28 17K 
[TXT]Indexed-container.html 06-Sep-2017 22:28 314K 
[TXT]Indexed-container.Co..>06-Sep-2017 22:28 597K 
[TXT]H-level.html 06-Sep-2017 22:28 40K 
[TXT]H-level.Truncation.html06-Sep-2017 22:28 573K 
[TXT]H-level.Truncation.P..>06-Sep-2017 22:28 210K 
[TXT]H-level.Closure.html 06-Sep-2017 22:28 307K 
[TXT]Groupoid.html 06-Sep-2017 22:28 49K 
[TXT]Function-universe.html 06-Sep-2017 22:28 1.4M 
[TXT]Fin.html 06-Sep-2017 22:28 89K 
[TXT]Expansion.html 06-Sep-2017 22:28 89K 
[TXT]Expansion.Equational..>06-Sep-2017 22:28 45K 
[TXT]Expansion.Delay-mona..>06-Sep-2017 22:28 84K 
[TXT]Expansion.CCS.html 06-Sep-2017 22:28 323K 
[TXT]Equivalence.html 06-Sep-2017 22:28 657K 
[TXT]Equational-reasoning..>06-Sep-2017 22:28 68K 
[TXT]Equality.html 06-Sep-2017 22:28 863K 
[TXT]Equality.Tactic.html 06-Sep-2017 22:28 147K 
[TXT]Equality.Proposition..>06-Sep-2017 22:28 14K 
[TXT]Equality.Groupoid.html 06-Sep-2017 22:28 105K 
[TXT]Equality.Decision-pr..>06-Sep-2017 22:28 81K 
[TXT]Equality.Decidable-U..>06-Sep-2017 22:28 71K 
[TXT]Embedding.html 06-Sep-2017 22:28 63K 
[TXT]Double-negation.html 06-Sep-2017 22:28 39K 
[TXT]Delay-monad.html 06-Sep-2017 22:28 8.3K 
[TXT]Delay-monad.Weak-bis..>06-Sep-2017 22:28 324K 
[TXT]Delay-monad.Strong-b..>06-Sep-2017 22:28 47K 
[TXT]Delay-monad.Partial-..>06-Sep-2017 22:28 172K 
[TXT]Delay-monad.Expansio..>06-Sep-2017 22:28 209K 
[TXT]Bool.html 06-Sep-2017 22:28 69K 
[TXT]Bisimilarity.Weak.De..>06-Sep-2017 22:28 159K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 44K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 20K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 29K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 94K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 11K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 71K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 96K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 26K 
[TXT]Bisimilarity.Weak.Co..>06-Sep-2017 22:28 13K 
[TXT]Bisimilarity.Weak.Cl..>06-Sep-2017 22:28 3.6K 
[TXT]Bisimilarity.Weak.CC..>06-Sep-2017 22:28 135K 
[TXT]Bisimilarity.Weak.CC..>06-Sep-2017 22:28 287K 
[TXT]Bisimilarity.Up-to.html06-Sep-2017 22:28 23K 
[TXT]Bisimilarity.Up-to.C..>06-Sep-2017 22:28 244K 
[TXT]Bisimilarity.Up-to.C..>06-Sep-2017 22:28 23K 
[TXT]Bisimilarity.Step.html 06-Sep-2017 22:28 38K 
[TXT]Bisimilarity.Exercis..>06-Sep-2017 22:28 90K 
[TXT]Bisimilarity.Exercis..>06-Sep-2017 22:28 858K 
[TXT]Bisimilarity.Exercis..>06-Sep-2017 22:28 107K 
[TXT]Bisimilarity.Exercis..>06-Sep-2017 22:28 162K 
[TXT]Bisimilarity.Compari..>06-Sep-2017 22:28 86K 
[TXT]Bisimilarity.Coinduc..>06-Sep-2017 22:28 49K 
[TXT]Bisimilarity.Coinduc..>06-Sep-2017 22:28 119K 
[TXT]Bisimilarity.Coinduc..>06-Sep-2017 22:28 22K 
[TXT]Bisimilarity.Coinduc..>06-Sep-2017 22:28 26K 
[TXT]Bisimilarity.Classic..>06-Sep-2017 22:28 135K 
[TXT]Bisimilarity.Classic..>06-Sep-2017 22:28 6.2K 
[TXT]Bijection.html 06-Sep-2017 22:28 161K 
[TXT]Agda.css 06-Sep-2017 22:28 1.2K 
[TXT]Agda.Primitive.html 06-Sep-2017 22:28 19K 
[TXT]Agda.Builtin.Unit.html 06-Sep-2017 22:28 1.2K 
[TXT]Agda.Builtin.Size.html 06-Sep-2017 22:28 1.7K 
[TXT]Agda.Builtin.Nat.html 06-Sep-2017 22:28 18K 
[TXT]Agda.Builtin.List.html 06-Sep-2017 22:28 4.3K 
[TXT]Agda.Builtin.Equalit..>06-Sep-2017 22:28 2.3K 
[TXT]Agda.Builtin.Bool.html 06-Sep-2017 22:28 2.5K 

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

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

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

------------------------------------------------------------------------
-- 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

-- The classical definition of (strong) bisimilarity.

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

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

import Bisimilarity.Coinductive.General

-- A coinductive definition of (strong) bisimilarity.

import Bisimilarity.Coinductive
import Bisimilarity.Coinductive.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.Coinductive.Delay-monad

-- Some exercises and results from "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi, as well as other results.

import Bisimilarity.Exercises.Other.CCS
import Bisimilarity.Exercises.Classical.CCS
import Bisimilarity.Exercises.Coinductive.CCS
import Bisimilarity.Exercises.Coinductive.6-2-5

-- Up-to techniques for strong bisimilarity.

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

------------------------------------------------------------------------
-- 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 classical definition of weak bisimilarity.

import Bisimilarity.Weak.Classical

-- A coinductive definition of weak bisimilarity.

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

-- Another coinductive definition of weak bisimilarity.

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

-- A comparison of the classical definition of weak bisimilarity and
-- one of the coinductive ones.

import Bisimilarity.Weak.Comparison

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

import Bisimilarity.Weak.Coinductive.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 "other" definition of weak bisimilarity.

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

-- Up-to techniques for the delay monad and the "first" definition of
-- weak bisimilarity.

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

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

-- A coinductive definition of (strong) similarity.

import Similarity.Strong
import Similarity.Strong.Equational-reasoning-instances

-- Lemmas related to strong similarity for CCS.

import Similarity.Strong.CCS

-- A coinductive definition of weak similarity.

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

-- Up-to techniques.

import Similarity.Weak.Up-to