## User login## Navigation |
## Theory## Concurrent Pattern CalculusConcurrent Pattern Calculus by Thomas Given-Wilson, Daniele Gorla, and Barry Jay:
Barry Jay's Pattern Calculus has been discussed a few times here before. I've always been impressed with the pattern calculus' expressive power for computing over arbitrary structure. The pattern calculus supports new forms of polymorphism, which he termed "path polymorphism" and "pattern polymorphism", which are difficult to provide in other calculi. The closest I can think of would be a compiler-provided generalized fold over any user-defined structure. This work extends the pattern calculus to the concurrent setting by adding constructs for parallel composition, name restriction and replication, and argues convincingly for its greater expressiveness as compared to other concurrent calculi. He addresses some of the obvious concerns for symmetric information flow of the unification operation. By naasking at 2011-01-25 03:19 | Functional | Logic/Declarative | Parallel/Distributed | Theory | 1 comment | other blogs | 8414 reads
## Parametric Prediction of Heap Memory RequirementsParametric Prediction of Heap Memory Requirements, by Victor Braberman, Federico Fernandez, Diego Garbervetsky, Sergio Yovine:
We've briefly discussed analyses to predict heap usage here on LtU, but I can't seem to find them. Anyone with a reference handy, please post in the comments! ## Automatic Staged CompilationAutomatic Staged Compilation, doctoral dissertation of Matthai Philipose:
I haven't read through it all yet, but after a cursory skim it certainly looks interesting. By naasking at 2010-11-29 19:36 | Implementation | Theory | login or register to post comments | other blogs | 6712 reads
## Yacc is deadIn Yacc is dead (2010) Matthew Might and David Darais of the University of Utah, Salt Lake City...
It seems every problem in computer science can be solved with either one more level of indirection or a derivative. By James Iry at 2010-11-29 03:48 | Implementation | Theory | 28 comments | other blogs | 37709 reads
## Conservative LogicEdward Fredkin and Tommoasso Toffoli from the MIT Labratory for Computer Science present Conservative Logic...
This paper has a small discussion in a forum thread mostly saying the paper should be on the front page. ## Eff - Language of the FutureThis is just a series of blog posts so far, as far as I can tell. But Andrej Bauer's work has been mentioned here many times, I am finding these posts extremely interesting, and I'm sure I will not be alone. So without further ado... Programming With Effects. Andrej Bauer and Matija Pretnar.
By Matt Hellige at 2010-09-29 02:30 | Effects | Fun | Functional | Theory | 10 comments | other blogs | 32714 reads
## Formal Compiler Implementation in a Logical FrameworkHickey, Jason and Nogin, Aleksey and Granicz, Adam and Aydemir, Brian (2003) Formal Compiler Implementation in a Logical Framework. Technical Report. California Institute of Technology.
I don't understand the details of this paper, but the general approach of using rewriting for compilation (including passes such as closure conversion) is very interesting in itself. (Edit: As a bonus, the paper is derived from the literate MetaPRL sources.) (Edit: Oleg's applicative-order term rewriting system for code generation shows how simpler rewriting systems can be used in the context of compilation.) By Manuel J. Simoni at 2010-06-08 11:11 | Implementation | Theory | login or register to post comments | other blogs | 8171 reads
## Tropical SemiringsTropical Semirings, Jean-Ã‰ric Pin. Idempotency 1994.
In the previous post, Ohad Kammar asked for some more examples of why we should care about adjunctions, which reminded me of one of my favorite examples. You can understand solving many optimization problems as looking for a Galois connection between your problem and the tropical semiring. (Galois connections in general are one of the sources of the program derivation superpowers of the Squiggolists. So if you want to prove programs like Shin Cheng-Mu does, it's worth understanding!) ## The Structure of Authority: Why security is not a separable concernThe Structure of Authority: Why security is not a separable concern, by Mark S. Miller, Bill Tulloh, and Jonathan Shapiro:
An important overview of why security properties cannot be an after-thought for any platform, languages and operating systems included. To this end, the paper covers security properties at various granularities from desktop down to object-level granularity, and how object-capabilities provide security properties that are compositional, and permit safely composing mutually suspicious programs. A recent LtU discussion on achieving security by built-in object-capabilities vs. building security frameworks as libraries reminded me of this paper. Ultimately, the library approach can work assuming side-effects are properly controlled via some mechanism, ie. effect types or monads, but any solution should conform to object capability principles to maintain safe composition. An example of a capability-secure legacy/library approach is Plash (Principle of Least Authority SHell), which provides object-specific file system name spaces. Any library interface to the file system should mimic this file system virtualization, which effectively pushes side-effect control down to OS-level objects, and which is essential to safely composing mutually suspicious programs that access the file system. By naasking at 2010-04-26 15:27 | General | Software Engineering | Theory | 49 comments | other blogs | 13517 reads
## A Formal System For Euclid's ElementsA Formal System For Euclid's Elements, Jeremy Avigad, Edward Dean, and John Mumma. Review of Symbolic Logic, Vol. 2, No. 4, 2009.
Diagrammatic languages are a perennial favorite discussion topic here, and Euclid's proofs constitute one of the oldest diagrammatic languages around. And yet for hundreds of years (at least since Leibniz) people have argued about whether or not the diagrams are really part of a But was this necessary, or just a contingent fact of the logical machinery available to them? Avigad and his coauthors show the former point of view also works, and that you can do it with very basic proof theory (there's little here unfamiliar to anyone who has read Pierce's book). Yet it sheds a lot of light on how the diagrams in the Elements work, in part because of their very careful analysis of how to read the diagrams -- that is, what conclusion a diagram really licenses you to draw, and which ones are accidents of the specific figure on the page. How they consider these issues is a good model for anyone designing their own visual programming languages. |
## Browse archives## Active forum topics |

## Recent comments

3 hours 46 min ago

5 hours 50 min ago

7 hours 8 min ago

7 hours 54 min ago

8 hours 17 min ago

8 hours 27 min ago

9 hours 26 min ago

9 hours 47 min ago

10 hours 58 min ago

19 hours 32 min ago