Lambda the Ultimate

Deerfield Beach, Florida, January 3-6, 2009
http://lfcs.info/lfcs09/

The LFCS series provides an outlet for the fast-growing body of work in the logical foundations of computer science, e.g., areas of fundamental theoretical logic related to computer science. The LFCS series began with Logic at Botik, Pereslavl-Zalessky, 1989 and was co-organized by Albert R. Meyer (MIT) and Michael Taitslin (Tver), after which organization passed to Anil Nerode.

LFCS Topics. Topics of interest include, but are not limited to:
* constructive mathematics and type theory;
* logic, automata and automatic structures;
* computability and randomness;
* logical foundations of programming;
* logical aspects of computational complexity;
* logic programming and constraints;
* automated deduction and interactive theorem proving;
* logical methods in protocol and program verification;
* logical methods in program specification and extraction;
* domain theory logics;
* logical foundations of database theory;
* equational logic and term rewriting;
* lambda and combinatory calculi;
* categorical logic and topological semantics;
* linear logic;
* epistemic and temporal logics;
* intelligent and multiple agent system logics;
* logics of proof and justification;
* nonmonotonic reasoning;
* logic in game theory and social software;
* logic of hybrid systems;
* distributed system logics;
* mathematical fuzzy logic;
* system design logics;
* other logics in computer science.

Proceedings will be published in the LNCS series. There will be a post-conference volume of selected works published in the Annals of Pure and Applied Logic.

Important Dates:
* Submission server available: September 1, 2008
* Submissions deadline (firm): September 14, 2008
* Notification: October 5, 2008
* Final papers for proceedings: October 15, 2008
* Symposium dates: January 3 - 6, 2009

I'm wondering if there are language implementations that (elegantly?) combine what Scala (at least) refers to as "higher-order type constructor polymorphism" with the code specialization capabilities of C++ style templates?

I don't mean the notion of "specialization" sometimes used to generically describe how instantiating a template List[int] will (likely) generate new code.

I mean programmer driven template specialization.

That's pretty much the question, so now I'll make a fool of myself trying to come up with an example.

class Vector[T](size:int, init:T) extends Sequence[T]
with Indexed[T]
with Iterable[T, Vector[X]]
{
/* stuff */
}

So Iterable, say, has methods like map and friends that will now return Vector[U] for some function (T => U). And all the Iterator and Builder machinery comes out nicely typed. Yada yada yada.

Now, it would be *really* nice to somehow be able to implement bit vectors with custom code. Making up a silly keyword:

specialize class Vector[Bool](....
{
/* Do NOT want to use the normal machinery here. */
}

We don't really want a vector of 32 bit Bool values! We want some custom bitwise code over an array of bytes or unsigned ints or something. We'll also need specialized Iterators[Vector[Bool]] (hopefully inlined) and associated machinery.

But in the end we get a usable bit vector class (1) with much better space/speed for Vector[Bool] and (2) we can still write code like this.

def somefun(vi:Vector[Int]): Vector[Bool] = vi.map((_ % 2 == 0));

Just a dumb and obvious example. We could also inquire about method (or function) specializations on values yada yada yada.

Hence my question - are there language implementations that nicely combine their elegant type systems with the power of template style code specialization?

Sorry if this is too implementation oriented a question.

Scott

Hi,
I'm trying to get SWI-Prolog and C to work together on MacOS 10.4.11 (Tiger) using the Prolog's Foreign Interface. Unfortunately I'm not an expert in either Prolog, or C, so I would appreciate some help.

It seems that there are some issues with the foreign function interface specifically on MacOS. The Prolog manual has a very nice example of how to use FFI with C (http://gollem.science.uva.nl/SWI-Prolog/Manual/foreignxmp.html)... which this doesn't work for me on MacOS, but worked fine under Linux (Ubuntu 8.04 Hardy).

I don't understand what's wrong with 'strlen' initially:

$ gcc -I/opt/local/lib/swipl-5.6.15/include -fpic -c lowercase.c
lowercase.c:1: warning: -fpic is not supported; -fPIC assumed
lowercase.c: In function 'pl_lowercase':
lowercase.c:14: warning: incompatible implicit declaration of built-in function 'strlen'

... and even though we do get an object file in the end, we can't create (and register?) a library at the next step (this seems to be the MacOS-specific problem):

$ gcc -shared -o lowercase.so lowercase.o
i686-apple-darwin8-gcc-4.0.1: unrecognized option '-shared'
/usr/bin/ld: Undefined symbols:
_main
_PL_get_atom_chars
_PL_register_foreign
_PL_unify_atom_chars
_PL_warning
collect2: ld returned 1 exit status

Any suggestions? I couldn't find anything online except http://www.phil.uu.nl/~xges/HOWTO/swipldynlib.html which seems quite old? Should I go for it anyway?

Thank you,
-- Georgi

It is generally known that JavaScript supports a functional style of programming. But because it does not have algebraic data types, the functional programming is usually limited to some simple higher order functions applied to Arrays.

I have often build small libraries that allow working with some aspects of algebraic data types in JavaScript. This time I thought is was cool enough to write a bit about it:

Algebraic Data Types in JavaScript

It includes:

• a very small footprint
• unfold, map and fold over any adt
• merging (read deforestation/fusion) of unfold, map and fold
• user defined derived properties (think derived classes Show, Eq...)

I also show how to do the Data Types à la carte style of Wouter Swierstra with this library.

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.

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.

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

Ehud recently lamented the lack of small interpreters for people to play with. I thought I would take this as an invitation share my JavaScript version of Cat that supports turtle graphics:

http://cat-language.com/interpreter.html

The parsing code will definitely make the angels weep and programmers gnash their teeth.

Enjoy!

Lots of times asking LTU is more effective than searching the ACM database (ie you guys are awesome!): Does anyone know of papers about flowchart layout algorithms? This could also be called 'automatic flowchart generation'. I've reviewed several commercial packages and it seems there are two approaches:


1) generate the flowchart as a directed graph and then feed it to graphviz dot to create a hierarchical layout with flowchart symbols


2) use a proper (proprietary?) algorithm to generate an aesthetically pleasing (dot fails in this regard) flowchart.


Searching the ACM database for 'flowchart layout' is problematic because it returns a LOT of results. Is anyone familiar with this type of algorithm?

Consider a language that provides lightweight concurrency primitives, like JoCaml or Erlang, and which uses co-operative threads like GNU Pth for this concurrency. A co-operative thread must explicitly yield to permit other threads to execute.

Has there been any research into some sort of inference for compiler-inserted yields? For instance, each co-operative thread has a "time slice" (or a "work slice"), and we would want the thread to yield after the slice has expired. In the limit, we can force each function call to decrement the "remaining slice" until it reaches zero, at which point we yield (I believe Erlang does this, or something similar). This would seem to be quite a heavy penalty though.

I was wondering if there was a "smarter" way, that didn't cost a repeated test and branch on every function call. For instance, the compiler could analyze the control flow, and insert checks every X function calls, where X > 1.

So is there any other way to build preemptive threading from co-operative threads, other than via timers, or the above technique of a runtime check per call?