Index of /~nad/listings/dependently-typed-syntax

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Data.Nat.html 08-Jun-2018 10:28 929  
[TXT]Agda.css 08-Jun-2018 10:28 1.2K 
[TXT]Agda.Builtin.Unit.html 08-Jun-2018 10:28 1.2K 
[TXT]Agda.Builtin.TrustMe..>08-Jun-2018 10:28 1.8K 
[TXT]Data.Empty.Irrelevan..>08-Jun-2018 10:28 1.9K 
[TXT]Data.Unit.Base.html 08-Jun-2018 10:28 1.9K 
[TXT]Data.Empty.html 08-Jun-2018 10:28 2.2K 
[TXT]Agda.Builtin.Equalit..>08-Jun-2018 10:28 2.3K 
[TXT]Agda.Builtin.Bool.html 08-Jun-2018 10:28 2.4K 
[TXT]Agda.Builtin.Sigma.html08-Jun-2018 10:28 2.7K 
[TXT]Level.html 08-Jun-2018 10:28 3.0K 
[TXT]Relation.Binary.EqRe..>08-Jun-2018 10:28 3.2K 
[TXT]Category.Monad.Ident..>08-Jun-2018 10:28 3.3K 
[TXT]Agda.Primitive.html 08-Jun-2018 10:28 3.8K 
[TXT]deBruijn.Context.html 08-Jun-2018 10:28 4.2K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 4.5K 
[TXT]Agda.Builtin.Strict...>08-Jun-2018 10:28 4.5K 
[TXT]Relation.Nullary.Pro..>08-Jun-2018 10:28 5.3K 
[TXT]Relation.Binary.Hete..>08-Jun-2018 10:28 5.8K 
[TXT]Universe.html 08-Jun-2018 10:28 6.1K 
[TXT]Relation.Nullary.html 08-Jun-2018 10:28 6.5K 
[TXT]Strict.html 08-Jun-2018 10:28 6.7K 
[TXT]README.html 08-Jun-2018 10:28 7.7K 
[TXT]Relation.Binary.Inde..>08-Jun-2018 10:28 8.5K 
[TXT]Category.Monad.html 08-Jun-2018 10:28 9.2K 
[TXT]Category.Functor.html 08-Jun-2018 10:28 9.2K 
[TXT]Relation.Binary.Prop..>08-Jun-2018 10:28 10K 
[TXT]Relation.Binary.Prop..>08-Jun-2018 10:28 10K 
[TXT]Data.Unit.html 08-Jun-2018 10:28 11K 
[TXT]Data.Bool.Base.html 08-Jun-2018 10:28 12K 
[TXT]Agda.Primitive.Cubic..>08-Jun-2018 10:28 15K 
[TXT]Data.Sum.html 08-Jun-2018 10:28 15K 
[TXT]Relation.Binary.Preo..>08-Jun-2018 10:28 17K 
[TXT]Function.Injection.html08-Jun-2018 10:28 17K 
[TXT]Agda.Builtin.Nat.html 08-Jun-2018 10:28 18K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 20K 
[TXT]Data.Sum.Base.html 08-Jun-2018 10:28 20K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 21K 
[TXT]Function.Bijection.html08-Jun-2018 10:28 23K 
[TXT]Relation.Binary.Inde..>08-Jun-2018 10:28 23K 
[TXT]Function.Surjection...>08-Jun-2018 10:28 26K 
[TXT]Category.Monad.Index..>08-Jun-2018 10:28 27K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 31K 
[TXT]Data.Maybe.Base.html 08-Jun-2018 10:28 35K 
[TXT]Category.Applicative..>08-Jun-2018 10:28 36K 
[TXT]Function.LeftInverse..>08-Jun-2018 10:28 36K 
[TXT]Function.Equality.html 08-Jun-2018 10:28 37K 
[TXT]Function.Equivalence..>08-Jun-2018 10:28 37K 
[TXT]Relation.Nullary.Dec..>08-Jun-2018 10:28 38K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 39K 
[TXT]deBruijn.Context.Ext..>08-Jun-2018 10:28 39K 
[TXT]Data.Maybe.html 08-Jun-2018 10:28 45K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 45K 
[TXT]Function.html 08-Jun-2018 10:28 47K 
[TXT]Function.Inverse.html 08-Jun-2018 10:28 51K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 53K 
[TXT]Data.Nat.Base.html 08-Jun-2018 10:28 54K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 58K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 58K 
[TXT]Relation.Binary.Cons..>08-Jun-2018 10:28 60K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 60K 
[TXT]Data.Product.html 08-Jun-2018 10:28 62K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 66K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 75K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 76K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 81K 
[TXT]Relation.Binary.Core..>08-Jun-2018 10:28 81K 
[TXT]Relation.Binary.Prop..>08-Jun-2018 10:28 86K 
[TXT]Relation.Unary.html 08-Jun-2018 10:28 88K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 93K 
[TXT]Relation.Binary.html 08-Jun-2018 10:28 97K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 103K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 121K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 136K 
[TXT]deBruijn.Context.Ext..>08-Jun-2018 10:28 137K 
[TXT]deBruijn.Context.Ext..>08-Jun-2018 10:28 139K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 147K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 148K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 154K 
[TXT]README.DependentlyTy..>08-Jun-2018 10:28 158K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 163K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 170K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 175K 
[TXT]deBruijn.Context.Ter..>08-Jun-2018 10:28 177K 
[TXT]deBruijn.Context.Bas..>08-Jun-2018 10:28 199K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 236K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 239K 
[TXT]deBruijn.Substitutio..>08-Jun-2018 10:28 271K 

README
------------------------------------------------------------------------
-- A library for working with dependently typed syntax
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- This library is leaning heavily on two of Conor McBride's papers:
--
-- * Type-Preserving Renaming and Substitution.
--
-- * Outrageous but Meaningful Coincidences: Dependent type-safe
--   syntax and evaluation.

-- This module gives a brief overview of the modules in the library.

module README where

------------------------------------------------------------------------
-- The library

-- Contexts, variables, context morphisms, context extensions, etc.

import deBruijn.Context

-- Parallel substitutions (defined using an inductive family).

import deBruijn.Substitution.Data.Basics

-- A map function for the substitutions.

import deBruijn.Substitution.Data.Map

-- Some simple substitution combinators. (Given a term type which
-- supports weakening and transformation of variables to terms various
-- substitutions are defined and various lemmas proved.)

import deBruijn.Substitution.Data.Simple

-- Given an operation which applies a substitution to a term,
-- satisfying some properties, more operations and lemmas are
-- defined/proved.
--
-- (This module reexports various other modules.)

import deBruijn.Substitution.Data.Application

-- A module which repackages (and reexports) the development under
-- deBruijn.Substitution.Data.

import deBruijn.Substitution.Data

-- Some modules mirroring the development under
-- deBruijn.Substitution.Data, but using substitutions defined as
-- functions rather than data.
--
-- The functional version of substitutions is in some respects easier
-- to work with than the one based on data, but in other respects more
-- awkward. I maintain both developments so that they can be compared.

import deBruijn.Substitution.Function.Basics
import deBruijn.Substitution.Function.Map
import deBruijn.Substitution.Function.Simple

-- The two definitions of substitutions are isomorphic (assuming
-- extensionality).

import deBruijn.Substitution.Isomorphic

------------------------------------------------------------------------
-- An example showing how the library can be used

-- A well-typed representation of a dependently typed language.

import README.DependentlyTyped.Term

-- Normal and neutral terms.

import README.DependentlyTyped.NormalForm

-- Instantiation of deBruijn.Substitution.Data for terms.

import README.DependentlyTyped.Term.Substitution

-- Instantiation of deBruijn.Substitution.Data for normal and neutral
-- terms.

import README.DependentlyTyped.NormalForm.Substitution

-- Normalisation by evaluation.

import README.DependentlyTyped.NBE

-- Various equality checkers (some complete, all sound).

import README.DependentlyTyped.Equality-checker

-- Raw terms.

import README.DependentlyTyped.Raw-term

-- A type-checker (sound).

import README.DependentlyTyped.Type-checker

-- An observation: There is a term without a corresponding syntactic
-- type (given some assumptions).

import README.DependentlyTyped.Term-without-type

-- Another observation: If the "Outrageous but Meaningful
-- Coincidences" approach is used to formalise a language, then you
-- can end up with an extensional type theory (with equality
-- reflection).

import README.DependentlyTyped.Extensional-type-theory

-- Inductively defined beta-eta-equality.

import README.DependentlyTyped.Beta-Eta

-- TODO: Add an untyped example.