User loginNavigation 
Inferring algebraic effectsLogical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:
Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial. By Ohad Kammar at 20140927 23:16  Functional  Implementation  Paradigms  Semantics  Theory  8 comments  other blogs  8243 reads
LtU's new server
Lambda the Ultimate is now running on a new, faster, more reliable server. The old one is now, uh... pining for the fjords.
This should resolve the increasingly frequent outages we've seen recently.
Because the old server had started failing, we didn't have time to do as much quality control on the migration as we would have liked. If anyone notices any issues with the site, please comment in this thread.
Currently known issues:
Breaking the Complexity Barrier of Pure Functional Programs with Impure Data StructuresBreaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures by Pieter Wuille and Tom Schrijvers:
This paper is along the same lines a question I asked a couple of years ago. The idea here is to allow programming using immutable interfaces, and then automatically transform it into a more efficient mutable equivalent. Inside the Wolfram LanguageVideo of Stephen Wolfram showing off the Wolfram Language and sharing his perspective on the design of the language at Strange Loop conference. What's in store for the most widely used language by discerning hackers?Or, in other words, what's the future of Emacs Lisp (and unavoidable HN discussion). The original message contains some interesting tidbits. I am not sure how the discussion on emacsdevel will develop. But speculating about things such as Guile elisp is, of course, our bailiwick. An operational and axiomatic semantics for nondeterminism and sequence points in CIn a recent LtU discussion, naasking comments that "I always thought languages that don't specify evaluation order should classify possibly effectful expressions that assume an evaluation order to be errors". Recent work on the C language has provided reasonable formal tools to reason about evaluation order for C, which has very complex evaluationorder rules. An operational and axiomatic semantics for nondeterminism and sequence points in C
One aspect of this work that I find particularly interesting is that it provides a program (separation) logic: there is a set of inference rules for a judgment of the form \(\Delta; J; R \vdash \{P\} s \{Q\}\), where \(s\) is a C statement and \(P, Q\) are logical pre,postconditions such that if it holds, then the statement \(s\) has no undefined behavior related to expression evaluation order. This opens the door to practical verification that existing C program are safe in a very strong way (this is all validated in the Coq theorem prover). Luca Cardelli FestschriftEarlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Hopefully the videos will be posted soon. By Ohad Kammar at 20140912 10:10  Category Theory  Lambda Calculus  Misc Books  Semantics  Theory  Type Theory  4 comments  other blogs  4752 reads
Rethinking PrologA recent paper by Oleg Kiselyov and Yukiyoshi Kameyama at the university of Tsukuba discusses weaknesses and areas for improvement to Prolog.
The paper mentions the strength of the approach used by miniKanren (which embeds logic programming with fairer search strategy than normal Prolog into Scheme) and Hansei (which embeds probability based nondeterminism into Ocaml using delimited continuations to allow directstyle expression of monadic code). After motivating some choices by studying the prototypical example of running append backwards they cover running parsers with "maximal munch" rule backwards  something that cannot be (declaratively) expressed in prolog. A very interesting paper on logic programming! It also thanks Tom Schrijvers of CHR fame at the end. Scratch jrScratch jr is an iPad version of the Scratch environment, designed with young kids in mind. It is the best kidoriented programming tool I tried so far, and my five year old has great fun making "movies" with it. As I noted on twitter an hour after installing, the ability to record your own voice and use it for your sprites is a killer feature. Check it out! Scala woes?A fork in the back? See discussion over at HN. People in the know are encouraged to shed light on the situation. 
Browse archivesActive forum topics
New forum topics

Recent comments
9 hours 5 min ago
1 day 19 hours ago
1 day 20 hours ago
2 days 17 hours ago
2 days 20 hours ago
2 days 20 hours ago
5 days 25 min ago
5 days 11 hours ago
5 days 12 hours ago
5 days 12 hours ago