Lambda the Ultimate

Hi, I have a problem with OpenGL in LispWorks. It's functional, cause the icosahedron example is functional. But I don't know, how I can draw... I explain it: I'd like to programming in OpenGL by Lisp. I make CAPI INTERFACE and OpenGL pane in. When I evaluate (capi:display (make-instance 'my-interface)) the window shows up. I make triangle:
(defun triangle()
(opengl:gl-begin opengl:*gl-polygon*)
(opengl:gl-vertex4-i 1 0 0 1)
(opengl:gl-vertex4-i 0 1 0 1)
(opengl:gl-vertex4-i 0 0 1 1)
(opengl:gl-end))
and now I'd like to drawing it on OpenGL canvas in my-interface. How can I do it?
(sorry for my explanation... I hope u get on :) ).

Termination Checking with Types, Andreas Abel. 2004.

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces lambda+mu, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

Recently on LtU, there has been a good deal of discussion about total functional programming, so I thought I'd link to an article that shows how to use typing to enforce termination. The main advantage of type-based approaches (as compared to analyzing the program text directly) is that the termination check is not as sensitive to the precise shape of the program; for example, you can beta-reduce a term and not alter whether the system thinks the program will terminate or not.

This paper is also nice because it provides a relatively simple example of bidirectional type checking, which is an important idea both practically (it reduces spurious type annotations and helps produce better error messages) and theoretically (it is intimately related to cut elimination).