User loginNavigation |
TheoryDecidability of Higher Order MatchingDecidability of Higher Order Matching, Colin Stirling.
This paper is very technical, but I think it's a problem of significant interest, since decidable fragments of higher-order unification are very important to theorem proving systems. As an aside, Huet conjectured that higher order matching was decidable in 1976, so it's taken thirty years of effort to prove this. Modular Verification of Assembly Code with Stack-Based Control AbstractionsModular Verification of Assembly Code with Stack-Based Control Abstractions by Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni Published in Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006. ©2006 ACM.
Of interest to those interested in verification, and the formal theory of stacks. Anyone else interested in seeing a new category created for assembly and intermediate languages? Church’s Thesis and Functional ProgrammingDavid Turner gives a condensed summary of the lambda calculus and functional programming in this paper on Church’s Thesis and Functional Programming. The lambda-calculus, which Church developed during the period of convergence from which the Thesis emerged, has influenced almost every aspect of the development of programming and programming languages. It is the basis of functional programming, which after a long infancy is entering adulthood as a practical alternative to traditional ad-hoc imperative programming languages. Many important ideas in mainstream programming languages—recursion, procedures as parameters, linked lists and trees, garbage collectors — came by cross fertilization from functional programming. Moreover the main schools of both operational and denotational semantics are lambda-calculus based and amount to using functional programming to explain other programming systems.Many of the PLT topics mentioned on LtU are covered - PLT in 20 pages or less. I'm still hoping for someone to publish a pop-PLT book that takes something like these 20 pages and turns them into a 800 page novel. In the meantime, this is a nice roadmap for PLT that helps provide the connections between such things as Curry-Howard, Coq, System F. (About as close to a cheatsheet for LtU that I've come across). A Logic for Parametric PolymorphismA Logic for Parametric Polymorphism, Gordon Plotkin and MartÃn Abadi.
By neelk at 2007-04-13 22:27 | Category Theory | Lambda Calculus | Semantics | Theory | login or register to post comments | other blogs | 7480 reads
Separation Logic courses (Reynolds)For some reason (probably starting with the letter N), seperation logic was recently mentioned here a few times. Since this area may be relatively unknown to many readers, I thought the following two course web sites from John C. Reynolds may be of interest: Separation Logic (Spring 2004)
Current Research on Separation Logic (Spring 2005) RZ for Constructive Mathematics in ProgrammingRZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer. Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. I haven't read the paper yet, but the abstract reminded me of PADS. By Jim Apple at 2007-02-03 21:19 | DSL | Semantics | Theory | Type Theory | 3 comments | other blogs | 6060 reads
Annotated POPL 2007 ProgramPOPL 2007 is just around the corner, and the Little Calculist has taken time off from inventing Web 4.0 to track down all the papers available online, and collect them in an annotated program, Favourite titles: Proving That Programs Eventually Do Something Good, and Lazy Multivariate Higher-Order Forward-Mode AD. I have no idea what the later means, but I love the pile-up of jargon. Seminar: Classical vs. Quantum ComputationClassical versus Quantum Computation. John Baez. This fall, John Baez has been conducting a seminar on classical and quantum computation. So far they appear to have covered mostly foundations of classical computation (lambda calculus, CCCs, the fixed point theorem). It's interesting to see lambda calculus introduced to an audience already comfortable with category theory. Excellent lecture notes are available for each week with a bit of supporting material, and there have been blog posts for each class on The n-Category Cafe (the most recent one is here). The blog posts have some extra discussion, and comments, of course. The seminar continues in the spring and I'm sure people may want to follow along... By Matt Hellige at 2006-12-21 21:16 | Theory | login or register to post comments | other blogs | 5580 reads
Natural Deduction Reading for BeginnersThe most active members of LtU for the most part already have a solid foundation in logic. For the rest of us interested in language design, but who are not already logicians here is a brief reading list on logic, focusing on natural deduction, the preferred method of expressing type systems.
More experienced members of LtU may perhaps consider contributing to the discussion with comments on the suggested reading or alternative suggestions. [Edit: removed A History of Natural Deduction and Elementary Logic Textbooks by Jeff Pelletier and added several new links as suggested by Charles Stewart and falcon.] Second Life Faces Threat to its Virtual EconomySecond Life Faces Threat to its Virtual Economy
Related to this thread, especially my "Not Merely Predictable" post, as well as the various Lightweight Static Capabilities and Robust Composition threads. I'm absolutely convinced that a future language design will evolve to accomodate the development of distributed systems in which these kinds of issues are impossible to impose. Is it time to add an "object capability security" and/or "cooperation without vulnerability" (a great phrase from Mark Miller) category to LtU? By Paul Snively at 2006-11-15 15:45 | DSL | Software Engineering | Theory | 39 comments | other blogs | 14664 reads
|
Browse archives
Active forum topics
|
Recent comments
11 weeks 16 hours ago
15 weeks 2 days ago
16 weeks 6 days ago
16 weeks 6 days ago
19 weeks 4 days ago
24 weeks 2 days ago
24 weeks 2 days ago
24 weeks 5 days ago
24 weeks 5 days ago
27 weeks 3 days ago