## User login## Navigation |
## Semantics## A Monadic Framework for SubcontinuationsA Monadic Framework for Subcontinuations
## XQuery 1.0 and XPath 2.0 Formal Semantics - Last Call
(via Michael Rys)
This is a Last Call Working Draft. Comments on this document are due no later than 15 July 2005... I guess that those interested in this area know about this, and for others it is a bit too late to get involved, but at least it's good to know the status of the formal specification. ## On Evaluation Contexts, Continuations, and the Rest of Computation
Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.
On Evaluation Contexts, Continuations, and the Rest of Computation Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuations-as-evaluation-contexts are the defunctionalized representation of the continuation of a single-step reduction function and that continuations-as-the-rest-of-thecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single-step reducer. The only difference is how these evaluation contexts are interpreted: a â€˜plugâ€™ interpretation yields one-step reduction, whereas a â€˜refocusâ€™ interpretation yields evaluation. By Andris Birkmanis at 2005-06-08 13:45 | Lambda Calculus | Semantics | 1 comment | other blogs | 5112 reads
## From shift and reset to polarized linear logic
By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chung-chieh Shan will be interesting to many who loves logic and Curry-Howard isomorphism.
From shift and reset to polarized linear logic Abstract: Griffin pointed out that, just as the pure lambda-calculus corresponds to intuitionistic logic, a lambda-calculus with first-class continuations corresponds to classical logic. We study how first-class delimited continuations, in the form of Danvy and Filinskiâ€™s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinskiâ€™s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuation-passing-style (CPS) transform: any pure lambda-term with an appropriate type is beta-eta-equivalent to the CPS transform of some shift-reset expression. We conclude that the lambda-calculus with shift and reset and the pure lambda-calculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambda-calculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambda-Âµ-calculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in call-by-value and call-byname settings. By Andris Birkmanis at 2005-06-06 19:17 | Functional | Lambda Calculus | Semantics | Type Theory | 15 comments | other blogs | 9728 reads
## The Essence of Data Access in Cw
The Essence of Data Access in Cw, The power is in the dot! Gavin Bierman, Erik Meijer, and Wolfram Schulte.
In this paper we concentrate on the data dimension. Our aim is to describe the essence of these extentions; by which we mean we identify, exemplify and formalize their essential features. Our tool is a small core language FCw, which is a valid subset of the full Cw language... we are able to formalize the type system and operational semantics of the data access fragments of Cw. If you have been following the discussions here of Cw, you already know about the language features discussed here, since the paper doesn't introduce new features. If you haven't seen Cw, section 2 is a short and readable introduction. The rest of the paper is more formal, and unless you need to prove formal results regarding Cw, might not be all that interesting. It won't hurt to keep in mind that it exists, since some of us may need something like FCw at one point or another. By Ehud Lamm at 2005-05-28 09:07 | Semantics | Type Theory | XML | login or register to post comments | other blogs | 6055 reads
## Nick Benton: Simple Relational Correctness Proofs for Static Analyses and Program TransformationsWe show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although many program analyses are traditionally formulated in very intensional terms, the associated transformations are actually enabled by more liberal extensional properties. We illustrate our approach with formal systems for analysing and transforming while-programs. The first is a simple type system which tracks constancy and dependency information and can be used to perform dead-code elimination, constant propagation and program slicing as well as capturing a form of secure information flow. The second is a relational version of Hoare logic, which significantly generalizes our first type system and can also justify optimizations including hoisting loop invariants. Finally we show how a simple available expression analysis and redundancy elimination transformation may be justified by translation into relational Hoare logic. Not really exciting as such, but this technical report version of the POPL 2004 paper includes most of the proofs, which some might find helpful. By Ehud Lamm at 2005-02-24 13:55 | Implementation | Semantics | 2 comments | other blogs | 4647 reads
## Barbara Partee: Reflections of a Formal Semanticist as of Feb 2005What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself. This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25... No surprise, really, if you follow the links we give here from time to time about TLGs and such. By Ehud Lamm at 2005-02-15 10:37 | History | Lambda Calculus | Semantics | Type Theory | 5 comments | other blogs | 9378 reads
## Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc
Oleg's presentation at the workshop in honor of Daniel Friedman is great fun as usual.
The topic of repeated applications of call/cc has been mentioned on LtU previously, a few years
ago. New this time: the full and correct beta-normalizer written as a
direct-style syntax-rule. The normalizer implements calculus of
explicit substitutions. The talk presents probably the shortest (and
the fastest) normal-order beta-normalizer as a (stand-alone) Scheme
macro. Another new feature is the discussion of self-applications of
delimited continuation operators. The talk mentions incidentally that
shift, control, shift0 and other, less-delimited control operators are the members of the same family: gshift/greset.
Hot stuff. By Ehud Lamm at 2005-01-19 13:07 | Lambda Calculus | Meta-Programming | Semantics | 1 comment | other blogs | 6913 reads
## The Four QuestionsPage 4 of the lecture notes from Mitch Wand's first Principles of Programming Languages lecture:
What do you consider the fundamental properties of a programming language? By Dave Herman at 2005-01-09 00:13 | Semantics | Teaching & Learning | 23 comments | other blogs | 9803 reads
## Denotational Semantics: A Methodology for Language Development
Denotational Semantics: A Methodology for Language Development. David Schmidt, Kansas State University.
I don't recall seeing this book mentioned on LtU before. The entire book is online and seems quite detailed and understandable. Each chapter ends with exercises for the reader and suggested readings. Thanks, Henry! |
## Browse archives## Active forum topics |

## Recent comments

3 hours 21 min ago

3 hours 36 min ago

3 hours 47 min ago

4 hours 21 min ago

4 hours 39 min ago

6 hours 10 min ago

1 day 4 hours ago

1 day 11 hours ago

1 day 21 hours ago

1 day 23 hours ago