Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Branch: master
Commits on Jul 14, 2012
  1. Added a recursive definition for executing a small step.

    It returns TPHang if no small step can be executed.  This is currently
    not consistent with the inductive definition, which does not implement
    any handling of hanging excutions.
    The best way to fix this might be create a definition that clearly
    states, that a small step is only possible, if the result of applying
    smallstep to the expression is *not* TPHang.  Using this definition, it
    should be possible to show, that the inductive definition is consistent
    with the recursive definition of small steps.
Commits on Jul 9, 2012
  1. Added a few lemmas and the preservation theorem.

    Lemma 1: Γ ⊳ e :: τ ∧ Γ ⊳ e :: τ' ⇒ τ = τ',
    Lemma 2: Substitution preserves types if the identifier and the inserted
    expression have the same type
Commits on Jul 7, 2012
  1. Changed the implementation of type environments to simply prepend new…

    … entries
    This includes changing all the necessary proofs.  Additionally, I have
    created a new notation for expressing that an expression has a certain
    type in a given environment.  The notation is "env |> exp ::: tau" to
    indicate that exp has type tau in environment evn.
Commits on Jul 3, 2012
  1. Identifiers are now represented as pairs of a string (the identifiers…

    … name) and a unique number
    This makes it much easier to choose a new, unique identifier.
  2. Merge pull request #4 from n-chan/master

    Axiomatic version of smallsteps.
  3. @n-chan
Commits on Jul 1, 2012
  1. Changed the definition of small_steps to better handle values

    Additionally, added proofs for LET-EVAL and LET-EXEC.
  2. Merge pull request #3 from n-chan/master

    Introduced axiomatic version of typing (which will hopefully be easier to use ;-) see examples)
Commits on Jun 30, 2012
  1. @n-chan
  2. @n-chan
Commits on Jun 28, 2012
  1. Merge pull request #2 from n-chan/master

    Split into subfiles, some work on small steps.
  2. @n-chan

    Started some theorems that guarantee that small_steps implements the …

    n-chan authored
    …small steps from the script.
  3. @n-chan
  4. @n-chan

    Split project into subfiles.

    n-chan authored
Commits on Jun 27, 2012
  1. Merge pull request #1 from n-chan/master

    Consistency lemmas + bugfix
  2. @n-chan

    Added consistency lemmas for all defined boolean equalities. Fixed fo…

    n-chan authored
    …rgotten TP_var and TP_error cases in type_eq.
Commits on Jun 25, 2012
  1. added naive substitution

  2. Added representation of expressions

    Colin Benner authored
Something went wrong with that request. Please try again.