User loginNavigation 
TheoryA Tutorial on Proof Theoretic Foundations of Logic Programming
A Tutorial on Proof Theoretic Foundations of Logic Programming. Paola Bruscoli and Alessio Guglielmi. ICLP'03.
I just glanced through this tutorial, but since I know quite a few LtU readers are into proof theory, I thought I'd share the link. By Ehud Lamm at 20050320 22:17  Logic/Declarative  Theory  2 comments  other blogs  6730 reads
The POPLmark Challenge
(via TYPES)
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked proofs? To gauge progress in this area, we issue here a set of challenge problems, dubbed the POPLmark Challenge, chosen to exercise many aspects of programming languages that are known to be difficult to formalize. A valid solution to the challenge will consist of appropriate software tools, a language representation strategy, and a demonstration that this infrastructure is sufficient to formalize the challenge problems. The POPLmark team explains,
We are not ourselves automated reasoning experts but rather potential users; our impression is that current tools are almost at the point where they can be used routinely. It's time to bring mechanized metatheory to the masses  go to it! A New Approach to Abstract Syntax with Variable BindingPitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001. In the lambda calculus, the particular choice of variable names  even free variables  is irrelevant. Names serve two purposes:
In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with captureavoiding substitution, the Barendregt variable convention,
There are several standard ways to deal with this. Generating fresh names with This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOASlike notation for introducing binders into an abstract syntax. This is the settheoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past. By Dave Herman at 20050314 15:53  Lambda Calculus  MetaProgramming  Theory  7 comments  other blogs  7650 reads
Linear ForwardersLinear forwarders are actually the basic mechanism of an earlier implementation of the pi calculus called the fusion machine. We modify the fusion machine, replacing fusions by forwarders. The result is more robust in the presence of failures, and more fundamental. And also: The point of this paper is to solve the problem of input capability with a language that is â€œjust rightâ€ â€“ it neither disallows more features than necessary (as does the join calculus), nor adds more implementation work than is necessary (as does the fusion machine). Yes, these are the same capabilities as in capabilitybased security. I am looking forward to read the complete paper, as it seems to confirm my unclear ideas of how capabilities and various pi calculi are related. By Andris Birkmanis at 20050308 13:58  Parallel/Distributed  Theory  2 comments  other blogs  5564 reads
μABC: A Minimal Aspect Calculus
Aspectoriented programming is emerging as a powerful tool for system design and development. In this paper, we study aspects as primitive computational entities on par with objects, functions and hornclauses. To this end, we introduce μABC, a namebased calculus, that incorporates aspects as primitive. In contrast to earlier work on aspects in the context of objectoriented and functional programming, the only computational entities in μABC are aspects. We establish a compositional translations into μABC from a functional language with aspects and higherorder functions. Further, we delineate the features required to support an aspectoriented style by presenting a translation of μABC into an extended πcalculus. Proof and Counterexample
Greg Restall is
writing a book, entitled Proof and Counterexample (or PnC for short). It's on logic viewed through the lens of proof theory. In particular, it covers natural deduction, sequent calculus, normalisation and cutelimination. It's designed to both be stateoftheart reseearch on these topics, together with an introduction appropriate for an advanced undergraduate. (We'll see how that works. I'll be testdriving the material with honours students from February to June in 2005.) Newcomers to the field might wonder why this is relevant to programming languages, and some readers would regard this as pointless theory... But if you are one of us guys excited by CurryHoward, you might enjoy this wiki a lot. The Kell Calculus
The Kell Calculus: A Family of HigherOrder Distributed Process Calculi
This paper presents the Kell calculus, a family of distributed process calculi, parameterized by languages for input patterns, that is intended as a basis for studying componentbased distributed programming. The Kell calculus is built around a picalculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higherorder communication, programmable membranes, and dynamic binding. The paper discusses these principles, and defines the syntax and operational semantics common to all calculi in the Kell calculus family. The paper provides a coinductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higherorder bisimulation called strong context bisimulation. The paper also contains several examples that illustrate the expressive power of Kell calculi. NB: a family of calculi, parameterized by languages See also: The Kell Calculus In this page you will find information about the current state of the Kell calculus, links to published papers and drafts, information about where the Kell calculus is going[...] By Andris Birkmanis at 20050214 08:55  Parallel/Distributed  Theory  1 comment  other blogs  14945 reads
Comparing the Expressive Power of the Synchronous and the Asynchronous picalculus
Comparing the Expressive Power of the Synchronous and the Asynchronous picalculus
The Asynchronous picalculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the picalculus which contains no explicit operators for choice and outputprefixing. The communication mechanism of this calculus, however, is powerful enough to simulate outputprefixing, as shown by Boudol, and inputguarded choice, as shown recently by Nestmann and Pierce. A natural question arises, then, whether or not it is possible to embed in it the full picalculus. We show that this is not possible, i.e. there does not exist any uniform, parallelpreserving, translation from the picalculus into the asynchronous picalculus, up to any â€œreasonableâ€ notion of equivalence. This result is based on the incapablity of the asynchronous picalculus of breaking certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the picalculus and CCS.Quite an important result for those who care about pi. The others may just enjoy the use of symmetry in the proof. As CiteSeer is down this weekend, I used a link to CiteBase. [on edit: CiteSeer is back] Principles of Program Analysis
To coincide with the reprinting of Principles of Program Analysis by
Flemming Nielson, Hanne Riis Nielson and Chris Hankin the authors launched a new web page containing lecture slides and other supplementary material.
The lecture slides cover things like data flow analysis, control flow analysis and abstract interpretation. By Ehud Lamm at 20050120 14:41  Theory  login or register to post comments  other blogs  6569 reads
Nondeterminism in functional languages
Nondeterminism in functional languages. Sondergaard and Sestoft. The Computer Journal, Volume 35, Issue 5, pp. 514523. 1992
The introduction of a nondeterministic operator in even an very simple functional programming language gives rise to a plethora of semantic questions. These questions are not only concerned with the choice operator itself. A surprisingly large number of different parameter passing mechanisms are made possible by the introduction of bounded nondeterminism. The diversity of semantic possibilities is examined systematically...A very useful paper if you are interested in this sort of thing. Thinking of nondeterminism helps calrify muddled thinking about properties such as referential transparency. The version I found online, alas, is a set of tiff image files, one for each page... By Ehud Lamm at 20050111 17:58  Functional  Theory  login or register to post comments  other blogs  4876 reads

Browse archivesActive forum topics 
Recent comments
1 week 7 hours ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 3 days ago