I am currently taking a course succinctly named "Computation and Deduction". In reality, this is the secret name for "Immense fun at graduate PL courses". The whole idea of the course is to get acquainted with the theorem representation system Twelf. Based upon the LF-theory, the idea is that one can represent programming languages and their property proofs in a way that ensures correctness. Computer Science proofs tend to be shallow. Usually, one has to run induction over something and most of the proof is just simple slavery to an operational semantics and its inversion rules. Hence, the proof system can usually be kept simple. Twelf is different from traditional proof assistants and theorem provers like Isabelle/HOL and Coq. The latter 2 systems has proof automation support in which the system can automate big parts of the proof. It tends to make easy work on all the boring cases. As it stands, the stable version of Twelf support representation only: You must explicitly write down your proof. However, this turns out to be fairly simple. Further, there is nothing in Twelf which disallows one to add proof automation to the system later. While I do not claim to be a master of Twelf at all, it is not that hard to wrap your head around. Consider this to be an overview of what Twelf is able to do for you. Many parts need further explanation than I provide here, but that may spark the curious mind to dig deeper into the world of Theorem Proving! Also take note that I may have errors in here. Hopefully it will be the case that further proof development will eliminate many of these. Here, we will develop a lambda calculus interpreter, curry style, extended with peano arithmetic (Since I want to add a type system later). What makes the lambda calculus so interesting as a model for computation? Turing completeness, simplicity and basis for functional languages ought to be compelling reasons and enough justification! In Twelf, one begins by declaring exp : type. which reads "exp is a type". "type" here is really the kind (*) symbol in disguise. Then we declare how lambda calculus expressions look syntactically: z : exp. s : exp -> exp. app : exp -> exp -> exp. lam : (exp -> exp) -> exp. Thats it! The symbol 'z' plays the role of zero. It is an expression. The symbol 's' is the successor operator, so when it is used one types 's E' for some expression E which we want the successor of. Hence it will have type 'exp -> exp'. Lambda application is 'app E1 E2'; our encoding of the classical '(E1 E2)' application. So when fed with 2 expressions, E1 and E2 , app will itself be an expression. Finally, the lambda abstraction. It is written as 'lam E' where E is of type 'exp -> exp'. One may wonder where the variables are hidden. The answer, curiously, is that we are using variables in Twelf to represent variables in our lambda calculus. A Lambda Calculus variable 'x' is just 'x' as a Twelf variable. This is clever since we don't have to define a set of variables and then use them in the language as one would have done in Coq. Further, it will become clear that we can get substitution for free by "borrowing" it from the Twelf host language. Again a case where we would had described it directly in Coq. We really do not need it right now, but it may be beneficial to declare what values are in our language. Values are computations which are finished and in due time, we don't want every possible stuck computation to be values. So let us be explicit and define values:

value : exp -> type.

value_z : value z.
value_s : value (s S)
           <- value S. 
value_lam : value (lam [x] E x).

We are declaring that 'value' is of type 'exp -> type'. This means that value is a type family, indexed by expressions. We can then go on and define the members of the type family. The 'value_z' symbol defines that 'z' is a value. The next rule uses an inductive argument: '(s S)' is a value under the assumption that 'S' is a value. Since we are using a capital S, Twelf's type checker will do its magic and infer the type of S. In Twelf variables in uppercase is free in the LF-term and is then treated universially by the system. The rules 'value_z' and 'value_s' together defines a system making all natural numbers into values. We finally address that lambda expressions are values. The notation '[x] E x' is a Twelf-lambda abstraction. in Haskell one would have written something like '\x -> E x' in SML it would have been 'fn x => E x'. This leaves us with the last leg of the journey, namely the semantics of the lambda calculus. The rules are defined as:

eval : exp -> exp -> type.
%mode eval +E -V.

eval_z : eval z z.
eval_s : eval (s S) (s S')
     <- eval S S'.
eval_app : eval (app E1 E2) V
     <- eval E1 (lam E1')
     <- eval E2 V'
     <- eval (E1' V') V.
eval_lam : eval (lam [x] E x) (lam [x] E x).

We define a relation on evaluations 'eval E V' where the pair (E, V) is in the relation if the expression E evaluates to V. The '%mode' line is mode information known from logic programming. We define that the first argument is an input and the second argument is an output. This restricts the way the relation is allowed to be used. Twelf will carry out a mode check, ensuring that our use of 'eval' is in accordance with this mode definition. While this is mostly used to ensure certain relations are total, we use it here as an extra check of sanity. If your rules doesn't even pass the mode check, something is definitely wrong. I had a typo originally and the mode check found that immediately since some capitalized free variables were not ground. The symbol 'z' evaluates to itself. In 'eval_s' we call inductively -- if we have '(s S)' and S evaluates to S', then we have (s S'). Lambda abstractions in the last line evaluate to themselves as well. This leaves us with the 'app' case. If E1 evaluates to a lambda abstraction '(lam E1')', E2 evaluates to V', and (E1' V') evaluates to V, then (app E1 E2) evaluates to V. NOTE: The cool thing here is that E1' is of type 'exp -> exp' so we can just apply V'. This is substitution for free! There is no need to define a separate substitution rule because we just borrow it from Twelf. At this point we can begin to play with our toy: add1 : exp = lam [x:exp] (s x). one = s z. two = s one. three = s two. These are straightforward definitions. One can then run queries prolog-style to find solutions to problems. In effect, we have a free interpreter for our language: %query 1 5 eval (app add1 one) V. Twelf outputs 'V = s (s z).' as expected. We have a lot of rough edges in the toy interpreter however, and we may even have bugs in it. But we will weed them out over the coming postings, when we begin to add proofs on top of the system. At the Twelf Website is a lot of tutorials written by the Masters. If this is interesting to you, it is recommended reading!