Lambda the Ultimate

Estasis have provided an approach to theorem proving, the Falso system, leveraging a very proof-theoretically strong axiomatic system - indeed the strongest possible in the tower of consistency strengths, far stronger than Woodin cardinals - together with elegant economy to provide highly compressed proof techniques. It is evidently much easier to prove theorems in this system than, for example, in Coq.

Past discussions here, such as On the (Alleged) Value of Proof for Assurance, show that the great speed-up in providing correctness proofs offered here is to be valued. I cannot bring myself to recommend this system too highly.

Dyalog has the pleasure of announcing the start of the 2011 edition of our International APL Programming Contest. The deadline for submissions this year is August 14th, 2011. The terms and conditions, and the tasks to be solved can be found at: http://www.dyalog.com/contest_2011

The First Prize winner can look forward to US$2,500 plus a round trip travel from anywhere in the world to the Dyalog '11 Conference in Boston Massachusetts, USA, during October 2-5 2011. In addition to the grand prize, second and third prizes will be awarded with US$1,200 and US$600 respectively and a further 20 contestants will receive $100 each.

Additionally, the people or organisations that introduce the winning students to the contest will receive the same dollar prizes – and they need not be students to make the introduction. This means that you (or if you prefer, your institution) will receive an amount equal to any prizes won by students that you have referred to the competition.

The purpose of the contest is specifically to encourage students and others to investigate APL; the organisers hope that participants will find that exposure to APL broadens their horizons and adds a new tool to their toolbox. A fully featured copy of the latest release of Dyalog APL is available free of charge to students, whether or not they wish to participate in the contest.

Students of other disciplines than Computer Science are also encouraged to participate: many of the most successful APL users have backgrounds in other sciences, and have found APL to be a “Tool of Thought” for expressing solutions to problems in a wide variety of fields. Last year, the competition was won by Ryan Tarpine, a computational biologist from Brown University. We would like to thank Ryan again this year, he has been instrumental in designing the 2011 problem set, and as a result we believe that the contest this year has the most interesting (and varied) set of tasks to date.

A total of US$12,600 in prize money has been provided by several sponsors, including US-based Fiserv, Italian based APL Italiana, Danish based SimCorp and UK-based Dyalog Ltd., as well as several anonymous individuals and companies.

In A Larger Decidable Semiunification Problem(2007), Brad Lushman and Gordon V. Cormack of University of Waterloo

[...] present a graph-theoretic framework in which to study instances of the semiunification problem (SUP), which is known to be undecidable, but has several known and important decidable subsets. One such subset, the acyclic semiunification problem (ASUP), has proved useful in the study of polymorphic type inference. We present graph-theoretic criteria in our framework that exactly characterize the ASUP acyclicity constraint. We then use our framework to find a decidable subset of SUP (which we call R-ASUP), which has a more natural description than ASUP, and strictly contains it.