Welcome to the nominal-workbench wiki!

You might want to read the coding style. The build system rules are described here. The test system is described here.

• data
• data/test
• data/test/run-fail - NoWork files that should run and fail
• data/test/run-pass - NoWork files that should run and succeed
• data/example
• doc
• src
• test - Test suite framework, it uses the files in data/test/

• Opam : chose your prefered way to do it
• opam install ocp-build (if ocp-build is keeped, will change otherwise)
• ...

• Project manager: Pierre Talbot
• Scrum master (1st iteration): Rémy Besognet
• Scrum master (2nd iteration): Rémy Besognet
• Scrum master (3rd iteration): Vincent Botbol
• Scrum master (4th iteration): Mathieu Chailloux

Main part:

• A first naive abstract syntax tree
• Typed terms
• Rewriting rules, including:
  • alpha-conversion
  • rules : pattern-matching
• [Rewriting Algorithm] (naïve)

Secondary part:

• Rewriting strategies
• Terms equivalence:
  • Commutativity
  • Associativity
  • "Floating binders"
• State space representation

1st : december, 17 2013 Summary

Nominal rewriting systems. Fernandez et al. http://gabbay.org.uk/papers/nomr.pdf

Locally nameless representation. Chargueraud. http://www.chargueraud.org/research/2009/ln/main.pdf

### Extensions

Challenge sur la gestion des langages à Binding http://homepages.inf.ed.ac.uk/rpollack/export/bindingChallenge_slides.pdf

Solution "locally nameless" du problème par Xavier Leroy (d'autres listés dans les slides) http://pauillac.inria.fr/~xleroy/publi/POPLmark-locally-nameless.pdf

For hash-consing over terms: Type-safe Modular Hash-Consing https://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf

The Maude system. Meseguer et al. http://maude.cs.uiuc.edu/

Wiki page on rewriting systems: http://en.wikipedia.org/wiki/Rewriting

The Stratego webpage about rewriting strategies: http://releases.strategoxt.org/strategoxt-manual/unstable/manual/chunk-chapter/stratego-rewriting-strategies.html

Specification Of Rewriting Strategies : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.1342&rep=rep1&type=pdf

Strategic pattern matching : http://www.st.ewi.tudelft.nl/~eelco/papers/Vis99.ps

Boolean operations

# term signatures :

constant True: Bool
constant 0 : Nat

operator Nat: Bool -> Bool
operator And: Bool * Bool -> Bool

# sample : And(True, Nat(True))

constant Nil : forall(A).List[A]
operator Cons : ...

# kind, every type has a kind

kind Nat : type
kind List : type => type
kind Var : atom 
	     ^ Nominal

Lambda-calcul

kind Term : type
kind Variable : atom

operator Var : Variable -> Term
operator App : Term * Term -> Term
operator Lambda : [Variable] * Term -> Term
operator Subst : [Variable] * Term * Term -> Term

rule [beta] :
  App(Lambda(?x, ?T), ?U)  => Subst(?x, ?T, ?U)
                  ^ pattern variable

rule [subst-var] :
  Subst(?x, Var(?x), ?T) => ?T

rule [subst-nvar] :
  Subst(?x, Var(?y), ?T) => Var(?y)

rule [app] :
  Subst(?x, App(?T, ?U), ?U) => App(Subst(?x, ?T, ?U), Subst(...))

rule [lambda] :
  Subst(,x, Lambda(?y, ?T), ?U) => Lambda(?y, Subst(?x, ?T, ?U))

Peano axioms:

kind Nat: type
constant 0 : Nat

operator Successor : Nat -> Nat
operator Add : Nat * Nat -> Nat

rule [add-nil-left] :
  Add(0, ?n) => ?n

rule [add] :
  Add(Successor(?u), ?v) => Successor(Add(?u, ?v))