Index of /~nad/listings/chi

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Values.html 04-Feb-2018 22:05 23K 
[TXT]Univalence-axiom.html 04-Feb-2018 22:05 565K 
[TXT]Termination.html 04-Feb-2018 22:05 5.6K 
[TXT]Tactic.By.html 04-Feb-2018 22:05 178K 
[TXT]Surjection.html 04-Feb-2018 22:05 50K 
[TXT]Size.html 04-Feb-2018 22:05 54K 
[TXT]Self-interpreter.html 04-Feb-2018 22:05 58K 
[TXT]Rices-theorem.html 04-Feb-2018 22:05 193K 
[TXT]Reflection.html 04-Feb-2018 22:05 119K 
[TXT]Reasoning.html 04-Feb-2018 22:05 21K 
[TXT]README.html 04-Feb-2018 22:05 4.8K 
[TXT]Propositional.html 04-Feb-2018 22:05 164K 
[TXT]Prelude.html 04-Feb-2018 22:05 124K 
[TXT]Preimage.html 04-Feb-2018 22:05 59K 
[TXT]Pointwise-equality.html04-Feb-2018 22:05 100K 
[TXT]Nat.html 04-Feb-2018 22:05 90K 
[TXT]Monad.html 04-Feb-2018 22:05 124K 
[TXT]Maybe.html 04-Feb-2018 22:05 44K 
[TXT]Logical-equivalence...>04-Feb-2018 22:05 20K 
[TXT]List.html 04-Feb-2018 22:05 59K 
[TXT]Interval.html 04-Feb-2018 22:05 74K 
[TXT]Internal-coding.html 04-Feb-2018 22:05 201K 
[TXT]Injection.html 04-Feb-2018 22:05 17K 
[TXT]Halting-problem.html 04-Feb-2018 22:05 232K 
[TXT]H-level.html 04-Feb-2018 22:05 38K 
[TXT]H-level.Truncation.html04-Feb-2018 22:05 552K 
[TXT]H-level.Truncation.P..>04-Feb-2018 22:05 197K 
[TXT]H-level.Closure.html 04-Feb-2018 22:05 292K 
[TXT]Groupoid.html 04-Feb-2018 22:05 45K 
[TXT]Function-universe.html 04-Feb-2018 22:05 1.4M 
[TXT]Free-variables.html 04-Feb-2018 22:05 288K 
[TXT]Fin.html 04-Feb-2018 22:05 150K 
[TXT]Equivalence.html 04-Feb-2018 22:05 647K 
[TXT]Equality.html 04-Feb-2018 22:05 819K 
[TXT]Equality.Tactic.html 04-Feb-2018 22:05 143K 
[TXT]Equality.Proposition..>04-Feb-2018 22:05 13K 
[TXT]Equality.Proposition..>04-Feb-2018 22:05 1.3K 
[TXT]Equality.Groupoid.html 04-Feb-2018 22:05 104K 
[TXT]Equality.Decision-pr..>04-Feb-2018 22:05 78K 
[TXT]Equality.Decidable-U..>04-Feb-2018 22:05 70K 
[TXT]Embedding.html 04-Feb-2018 22:05 62K 
[TXT]Double-negation.html 04-Feb-2018 22:05 37K 
[TXT]Deterministic.html 04-Feb-2018 22:05 20K 
[TXT]Constants.html 04-Feb-2018 22:05 17K 
[TXT]Computability.html 04-Feb-2018 22:05 223K 
[TXT]Compatibility.html 04-Feb-2018 22:05 42K 
[TXT]Combinators.html 04-Feb-2018 22:05 196K 
[TXT]Coding.html 04-Feb-2018 22:05 292K 
[TXT]Coding.Instances.html 04-Feb-2018 22:05 13K 
[TXT]Coding.Instances.Nat..>04-Feb-2018 22:05 1.5K 
[TXT]Chi.html 04-Feb-2018 22:05 39K 
[TXT]Cancellation.html 04-Feb-2018 22:05 16K 
[TXT]Bool.html 04-Feb-2018 22:05 66K 
[TXT]Bijection.html 04-Feb-2018 22:05 156K 
[TXT]Bag-equivalence.html 04-Feb-2018 22:05 344K 
[TXT]Atom.html 04-Feb-2018 22:05 36K 
[TXT]Agda.css 04-Feb-2018 22:05 1.2K 
[TXT]Agda.Primitive.html 04-Feb-2018 22:05 3.6K 
[TXT]Agda.Primitive.Cubic..>04-Feb-2018 22:05 14K 
[TXT]Agda.Builtin.Word.html 04-Feb-2018 22:05 1.6K 
[TXT]Agda.Builtin.Unit.html 04-Feb-2018 22:05 1.2K 
[TXT]Agda.Builtin.String...>04-Feb-2018 22:05 5.0K 
[TXT]Agda.Builtin.Size.html 04-Feb-2018 22:05 2.8K 
[TXT]Agda.Builtin.Reflect..>04-Feb-2018 22:05 78K 
[TXT]Agda.Builtin.Nat.html 04-Feb-2018 22:05 17K 
[TXT]Agda.Builtin.List.html 04-Feb-2018 22:05 3.5K 
[TXT]Agda.Builtin.Int.html 04-Feb-2018 22:05 3.0K 
[TXT]Agda.Builtin.Float.html04-Feb-2018 22:05 9.6K 
[TXT]Agda.Builtin.Equalit..>04-Feb-2018 22:05 2.2K 
[TXT]Agda.Builtin.Char.html 04-Feb-2018 22:05 3.3K 
[TXT]Agda.Builtin.Bool.html 04-Feb-2018 22:05 2.4K 

README
------------------------------------------------------------------------
-- A formalisation of one variant of the language χ, along with a
-- number of properties
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

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

module README where

-- Atoms.

import Atom

-- Various constants.

import Constants

-- A specification of the language χ.

import Chi

-- The semantics is deterministic.

import Deterministic

-- Values.

import Values

-- Some cancellation lemmas.

import Cancellation

-- "Reasoning" combinators.

import Reasoning

-- The abstract syntax is a set, and the semantics is propositional.

import Propositional

-- The "terminates" relation.

import Termination

-- Compatibility lemmas.

import Compatibility

-- Definitions of "free in" and "closed", along with some properties.

import Free-variables

-- Encoders and decoders.

import Coding

-- Encoder and decoder instances.

import Coding.Instances

-- Encoder and decoder instances for Atom.χ-ℕ-atoms.

import Coding.Instances.Nat

-- Internal coding.

import Internal-coding

-- Some χ program combinators.

import Combinators

-- Definition of the size of an expression, along with some
-- properties.

import Size

-- A self-interpreter (without correctness proof).

import Self-interpreter

-- Partial functions, computability.

import Computability

-- The halting problem.

import Halting-problem

-- Rice's theorem.

import Rices-theorem

-- A theorem related to pointwise equality.

import Pointwise-equality