Library Base

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

Library ARS

• Abstract Reduction Systems
• Interpolation
• Evaluation

Library Lvw

• Syntax of the weak call-by-value lambda calculus
• Notation using binders
• Important terms
• Substitution
• Important definitions
  • Alternative definition of closedness
• Reduction
• Properties of the reduction relation
  • Properties of the reflexive, transitive closure of reduction
• Equivalence
  • Properties of the equivalence relation
• Definition of convergence
• Eta expansion
• Useful lemmas

Library Tactics

• Tactics for closedness and abstractions
• Simplifying goals
• Solving reductions
• Solving equivalences

Library Bool

• Encoding of booleans
• Boolean And and Or

Library Nat

• Encoding of natural numbers
• Predecessor
• Addition
• Multiplication

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

• Inernalized Maybe type

Library Equality

• Equality of encoded natural numbers
• Equality of encoded terms

Library Subst

• Internalized Substitution

Library Size

• Internalized size of terms

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

• Definition of parallel or

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

• First Fixed Point Theorem
• Second Fixed Point Theorem

Library Proc

Library Scott

• Scott's Theorem
• Applications of Scott's Theorem

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
  • Rice's Theorem, classical
• 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