User loginNavigation 
SemanticsAchieving Security Despite Compromise Using ZeroKnowledgeAchieving Security Despite Compromise Using ZeroKnowledge
This is the followup to this story. The prior work did not account for compromised participants. This work does. I continue to be excited about the prospect of this previous story's work being applied to the type system described in this story, possibly resulting in an awesome new language for developing secure software. By Paul Snively at 20090507 20:20  Implementation  Semantics  Type Theory  2 comments  other blogs  5439 reads
Branching Time vs. Linear Time: Semantical PerspectiveSumit Nain and Moshe Vardi, Branching Time vs. Linear Time: Semantical Perspective, invited ATVA'07 paper.
In revisiting the notion of process equivalence, which is a fairly central part of concurrency theory, Nain and Vardi end up arguing in favor of a purely tracebased notion of equivalence and the use of lineartime logics. This in turn leads to a rejection of bisimulation as a tool for establishing process equivalences:
They take pains to point out that they are not claiming that bisimulation or CTL should be abandoned or are not useful. Rather their emphasis is on the fact that bisimulation is not a contextual equivalence and is therefore not appropriate for establishing equivalence between (for example) a specification and its implementation. As they say in the conclusion of the paper:
By Allan McInnes at 20090426 22:55  Parallel/Distributed  Semantics  26 comments  other blogs  10812 reads
Semantics of Memory Management for Polymorphic LanguagesIn Semantics of Memory Management for Polymorphic Languages (1997) Greg Morrisett and Robert Harper ...present a static and dynamic semantics for an abstract machine that evaluates expressions of a polymorphic programming language. Unlike traditional semantics, our abstract machine exposes many important issues of memory management, such as value sharing and control representation. We prove the soundness of the static semantics with respect to the dynamic semantics using traditional techniques. We then show how these same techniques may be used to establish the soundness of various memory management strategies, including typebased, tagfree garbage collection; tailcall elimination; and environment strengthening. This should keep the formal semantics LtUers happy for a little while. But is all the machinery necessary? Is there an easier way to prove that garbage can be thrown out? Denotational design with type class morphismsDenotational design with type class morphisms. Conal Elliott.
To continue in our new allConal format... This paper brings together a bunch of things that Conal's been talking about lately, and "algebra of programming" fans will probably like his approach. (I have a hunch that what he calls a "type class morphism" could be described using standard categorical jargon, but I haven't given it much thought. Suggestions?) By Matt Hellige at 20090219 21:35  Functional  Semantics  12 comments  other blogs  10231 reads
DanaLuke Palmer and Nick Szabo can shoot me for this if they want, but I think this is warranted, and I want to connect a couple of dots as well. Luke is one of a number of computer scientists, with Conal Elliott probably being the best known, who have devoted quite a bit of attention to Functional Reactive Programming, or FRP. FRP has been discussed on LtU off and on over the years, but, unusually for LtU IMHO, does not seem to have gotten the traction that some other similarly abstruse subjects have. In parallel, LtU has had a couple of interesting threads about Second Life's economy, smart contracts, usage control, denial of service, technical vs. legal remedies, and the like. I would particularly like to call attention to this post by Nick Szabo, in which he discusses a contract language that he designed:
In recent private correspondence, Nick commented that he'd determined that he was reinventing synchronous programming Ã la Esterel, and mentioned "Reactive" programming. Ding! To make a potentially long entry somewhat shorter, Luke is working on a new language, Dana, which appears to have grown out of some frustration with existing FRP systems, including Conal Elliot's Reactive, currently perhaps the lynchpin of FRP research. Luke's motivating kickoff post for the Dana project can be found here, and there are several followup posts, including links to experimental source code repositories. Of particularly motivating interest, IMHO, is this post, where Luke discusses FRP's interaction with garbage collection succinctly but nevertheless in some depth. Luke's most recent post makes the connection from Dana, which Luke has determined needs to have a dependentlytyped core, to Illative Combinatory Logic, explicit, and offers a ~100 line type checker for the core. I find this very exciting, as I believe strongly in the project of being able to express computation centered on time, in the sense of Nick's contract language, in easy and safe ways extremely compelling. I've intuited for some time now that FRP represents a real breakthrough in moving us past the Von Neumann runtime paradigm in fundamental ways, and between Conal Elliott's and Luke's work (and no doubt that of others), it seems to me that my sense of this may be borne out, with Nick's contract language, or something like it, as an initial application realm. So I wanted to call attention to Luke's work, and by extension recapitulate Conal's and Nick's, both for the PLT aspects that Luke's clearly represents, but also as a challenge to the community to assist in the realization of Nick's design efforts, if at all possible. By Paul Snively at 20090218 21:55  Functional  General  Implementation  Lambda Calculus  Semantics  Theory  Type Theory  17 comments  other blogs  12909 reads
A MachineChecked Model for a JavaLike Language, Virtual Machine, and CompilerG. Klein and T. Nipkow, A MachineChecked Model for a JavaLike Language, Virtual Machine, and Compiler, ACM TOPLAS, vol. 28, no. 4, 2006. This is a fairly lengthy article (clocking in at 77 pages), in part because it presents a wealth of technical detail. The authors state that the aim of the article "is to demonstrate the stateoftheart in machinechecked language definitions." For those who are curious, the Isabelle theories are available in the Archive of Formal Proofs. Parameterized Notions of ComputationParameterized Notions of Computation, Robert Atkey, JFP 2008.
Once you've programmed with monads for a while, it's pretty common to start defining parameterized families of monads  e.g., we might define a family of type constructors for IO, in which the program type additionally tracks which files the computation reads and writes from. This is a very convenient programming pattern, but the theory of it is honestly a little sketchy: on what basis do we conclude that the indices we define actually track what we intend them to? And furthermore, why can we believe that (say) the monadic equational laws still apply? That's the question Atkey lays out a nice solution to. He gives a nice categorical semantics for indexed, effectful computations, and then cooks up lambda calculi whose equational theory corresponds to the equations his semantics justifies. The application to delimited continuations is quite nice, and the type theories can also give a little insight into the basics of how stuff like Hoare Type Theory works (which uses parameterized monads, with a very sophisticated language of parameters). On a slightly tangential note, this also raises in my mind a methodological point. Over the last n years, we've seen many people identify certain type constructors, whose usage is pervasive, and greatly simplified with some syntactic extensions  monads, comonads, applicative functors, arrows, and so on. It's incredible to suggest that we have exhausted the list of interesting types, and so together they constitute a good argument for some kind of language extension mechanism, such as macros. However, all these examples also raise the bar for when a macro is a good idea, because what makes them compelling is precisely that the right syntax yields an interesting and pretty equational theory in the extended language. By neelk at 20090211 21:40  Category Theory  Lambda Calculus  Semantics  Type Theory  16 comments  other blogs  12308 reads
Verifying Compiler Transformations for Concurrent Programs
Verifying Compiler Transformations for Concurrent Programs. Sebastian Burckhardt, Madanlal Musuvathi, Vasu singh.
ompilers transform programs, either to optimize performance or to translate languagelevel constructs into hardware primitives. For concurrent programs, ensuring that a transformation preserves the semantics of the input program can be challenging. In particular, the emitted code must correctly emulate the semantics of the languagelevel memory model when running on hardware with a relaxed memory model. In this paper, we present a novel proof methodology for proving the soundness of compiler transformations for concurrent programs. Our methodology is based on a new formalization of memory models as dynamic rewrite rules on event streams. We implement our proof methodology in a firstofitskind semiautomated tool called Traver to verify or falsify compiler transformations. Using Traver, we prove or refute the soundness of several commonly used compiler transformations for various memory models. In this process, we find subtle bugs in the CLR JIT compiler and in the JSR133 Java JIT compiler recommendations. The goal is to reason about the effects that different memory models may have on the validity of transformations. Program execution is modeled as an event stream, with the memory model being able to alter the event stream by swapping or eliminating events. Each concurrent execution thread produces a separate event stream. The event stream produced by the execution of the concurrent program is the (possibly altered) result of merging the event streams of each component. The validity of transformation can thus be proved relative to a specific memory model (i.e., a set of stream rewrite rules). Traver lives here. By Ehud Lamm at 20090110 06:45  Implementation  Parallel/Distributed  Semantics  2 comments  other blogs  9509 reads
A Framework for Comparing Models of Computation
A Framework for Comparing Models of Computation by Edward A. Lee and Alberto SangiovanniVincentelli, 1998.
We give a denotational framework (a â€œmeta modelâ€) within which certain properties of models of computation can be compared. It describes concurrent processes in general terms as sets of possible behaviors. A process is determinate if, given the constraints imposed by the inputs, there are exactly one or exactly zero behaviors. Compositions of processes are processes with behaviors in the intersection of the behaviors of the component processes. The interaction between processes is through signals, which are collections of events. Each event is a valuetag pair, where the tags can come from a partially ordered or totally ordered set. Timed models are where the set of tags is totally ordered. Synchronous events share the same tag, and synchronous signals contain events with the same set of tags. Synchronous processes have only synchronous signals as behaviors. Strict causality (in timed tag systems) and continuity (in untimed tag systems) ensure determinacy under certain technical conditions. The framework is used to compare certain essential features of various models of computation, including Kahn process networks, dataflow, sequential processes, concurrent sequential processes with rendezvous, Petri nets, and discreteevent systems.The generality of the approach looks very impressive. Can anyone share firsthand experience with this framework? Would be great to see E compared to Oz! By Andris Birkmanis at 20080911 15:02  Parallel/Distributed  Semantics  5 comments  other blogs  6905 reads
Compiler Validation through Program AnalysisAnna Zaks and Amir Pnueli (2008). CoVaC: Compiler Validation by Program Analysis of the CrossProduct. In Proc. 15th Symp. Formal Methods. From the introduction:
and

Browse archivesActive forum topics 
Recent comments
16 hours 26 min ago
17 hours 15 min ago
1 day 11 hours ago
1 day 13 hours ago
1 day 13 hours ago
2 days 5 hours ago
2 days 6 hours ago
2 days 13 hours ago
3 days 11 hours ago
3 days 16 hours ago