Lambda the Ultimate

Let me apologize in advance for my poor English.

I'm looking for information about how to program a forex trading system with functional programming (I use scheme). Any idea or link you could give me?

Thanks

Parametric Higher-Order Abstract Syntax for Mechanized Semantics

We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and translation from a language with ML-style pattern matching to a simpler language with no variable-arity binding constructs. By avoiding the syntactic hassle associated with first-order representation techniques, we achieve a very high degree of proof automation.

I was aware of this some months ago now, but held back commenting on it at Adam's request until it had been accepted for publication, which it now apparently has. This is (one element of) Adam's continued work on LambdaTamer, his Coq-based environment for building certified compilers. There is a new version of LambdaTamer using this parametric higher-order abstract syntax approach. The new version also works in current and future versions of Coq, unlike the previous version. Finally, Adam is apparently working on a paper regarding "type-theoretic denotational semantics for higher order, impure object languages" and is post-docing with Greg Morrisett. The relationship between Adam's work and the YNot project is a bit unclear to me; perhaps either Adam or Greg could help clarify that.

Update: Whoops. I got ahead of myself and neglected to notice that the paper is not actually yet available, although the new version of LambdaTamer is. So at the moment, this story is merely to note that the paper exists and to provide a link to the new LambdaTamer. My apologies to Adam and the LtU readership.

2nd Update: The paper is now available at the link, in either PostScript or PDF form.

Dependent typing is very interesting, although perhaps it can be pretty complicated to understand and use and implement? An alterantive, from Rondon, Kawaguchi, Jhala: Liquid Types.

We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without paying the heavy price of of manual annotation.

I have some openings in my team for people interested in programming languages, compilers, Web programming, type systems, and all that good stuff:

• Software Development Engineer (232909)
• Software Development Engineer (232906)

Don't hesitate to contact me for more information.