## Library Base

- Base Library for ICL
- Iteration
- Decidability
- Lists
- Filter
- Element removal
- Duplicate-free lists
- Cardinality
- Power lists
- Finite closure iteration

## Library ARS

## Library Lvw

- Syntax of the weak call-by-value lambda calculus
- Notation using binders
- Important terms
- Substitution
- Important definitions
- Reduction
- Properties of the reduction relation
- Equivalence
- Definition of convergence
- Eta expansion
- Useful lemmas

## Library Tactics

## Library Bool

## Library Nat

## Library Encoding

- Size of terms
- Properties of the encoding for nat
- Encoding for terms
- Interalized encoding combinators
- Interalized encoding of natural numbers
- Interalized term encoding

## Library Options

## Library Equality

## Library Subst

## Library Size

## Library Seval

- Definition of evaluation
- Step indexed evaluation
- Equivalence between step index evaluation and evaluation
- Evaluation as a function
- Equivalence between the evaluation function and step indexed evaluation
- Omega diverges
- If an application converges, both sides converge

## Library Partial

## Library Eval

- Internalized Evaluation Function
- Correctness of the internalized evaluation function
- Internalized Evaluation

## Library Por

## Library Decidability

- Definition of decidability in \lambda_vw
- Complement, conj and disj of predicates
- Deciders for complement, conj and disj of ldec predicates
- Decidable predicates are closed under complement, conj and disj

## Library Fixpoints

## Library Proc

## Library Scott

## Library Acceptability

- Definition of acceptance and semi decidablity
- Properties of acceptance
- Semi-ldec predicates are closed under conj and disj
- Decidable predicates are semi-ldec (and their complement too)

## Library Rice

- The self halting problem is not semi-ldec
- Rice's Theorem
- Applications of Rice's Theorem
- Rice's Theorem, classical, on combinators

## Library Computability

## Library bijection

## Library Enum

## Library Lists

## Library EnumInt

## Library Markov

## Library RE

- Definition of Recursive Enumerability
- The Enumeration combinator and its properties
- Recursive Enumerability implies semi decidability
- Semi decidability implies recursive enumerability

## Library AD

## Library DA

## Library MoreAcc

## Library Pairs

This page has been generated by coqdoc