StringBase

BaseLists

Size

• Internalized size of terms

internalize_demo

Lists

LProd

LProp

LBool

• Encoding of booleans

Subst

• Internalized Substitution

internalize_tac

Base

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

Encoding

• Encoding for terms
• Interalized encoding of natural numbers
• Interalized term encoding

ARS

• Abstract Reduction Systems, from Semantics Lecture at Programming Systems Lab, https://www.ps.uni-saarland.de/courses/sem-ws13/

LTactics

Reflection

crush_no_refl_ideas

Tactics_old

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

SumBool

intermediate

internalize_def

LOptions

• Inernalized Maybe type

LvwClos_Eval

Lvw

• Syntax of the weak call-by-value lambda calculus
• Notation using binders
• Important terms
• Substitution
• Important definitions
• Size of terms
  • 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

LvwClos

• • Properties of the extended reduction relation
  • Properties of the equivalence relation

LNat

• Encoding of natural numbers

Equality

• Equality of encoded natural numbers
• Equality of encoded terms

bijection

Proc

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