Madison

A programming language in the genre of dsl by Chris Pressey, Cat's Eye Technologies, Dec 2, 2011

Madison is a language in which one can state proofs of properties of term-rewriting systems. Classical methods of automated reasoning, such as resolution, are not used; indeed, term-rewriting itself is used to check the proofs. Both direct proof and proof by induction are supported. Induction in a proof must be across a structure which has a well-founded inductive definition. Such structures can be thought of as types, although this is largely nominal; the traditional typelessness of term-rewiting systems is largely retained.

Sample Program

type tree is
  tree(leaf)        -> true
  tree(branch(X,Y)) -> and(tree(X),tree(Y))
in let
  reflect(leaf)        -> leaf
  reflect(branch(A,B)) -> branch(reflect(B),reflect(A))
in theorem
  forall X where tree(X)
    reflect(reflect(X)) ~> X
proof
  case X = leaf
    reflect(reflect(leaf))
    -> reflect(leaf)        [by reflect.1]
    -> leaf                 [by reflect.1]
  case X = branch(S, T)
    reflect(reflect(branch(S, T)))
    -> reflect(branch(reflect(T),reflect(S)))          [by reflect.2]
    -> branch(reflect(reflect(S)),reflect(reflect(T))) [by reflect.2]
    -> branch(S,reflect(reflect(T)))                   [by IH]
    -> branch(S,T)                                     [by IH]
qed

Computational Class

believed Turing-complete

Programming Paradigms

Defined by

Specs on Spec distribution