User loginNavigation 
SemanticsA Typetheoretic Foundation for Programming with Higherorder Abstract Syntax and Firstclass Substitutions
A Typetheoretic Foundation for Programming with Higherorder Abstract Syntax and Firstclass Substitutions by Brigitte Pientka, appeared in POPL 08.
Higherorder abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as captureavoiding substitution and renaming. This is achieved by representing binders in the objectlanguage via binders in the metalanguage. However, enriching functional programming languages with direct support for HOAS has been a major challenge, because recursion over HOAS encodings requires one to traverse  abstractions and necessitates programming with open objects.Its been a while since I posted, but this paper appears that it may be of interest to some members of this community. It looks interesting to me, but I just wish I understood all the terminology. I don't know what "open objects" are, and why they are a problem. I don't understand what HOAS is. I don't even know what binders are. The list goes on. I surely can't be the only person who is interested, but feels that this is just out of their grasp. I bet that I probably could understand these things with a minimum of explanation, given I have experience implementing languages. If anyone is interested in rephrasing the abstract in more basic terms, I would be very appreciative. [Edit: corrected spelling of Brigitte Pientka. My apologies.] By cdiggins at 20091003 18:51  Functional  Semantics  Theory  26 comments  other blogs  14896 reads
A Veriï¬ed Compiler for an Impure Functional LanguageA Veriï¬ed Compiler for an Impure Functional Language
The latest from Adam Chlipala. Yet another evolutionary step for Lambda Tamer. Between this and Ynot the Coq/certified compiler story seems to be getting more impressive nearly daily. By Paul Snively at 20090810 16:09  Functional  Implementation  Lambda Calculus  Semantics  8 comments  other blogs  8968 reads
LNGen
There are really three stories here:
From the U. Penn folks who brought us the Coq tutorial at POPL '08. By Paul Snively at 20090507 20:28  Implementation  Semantics  Software Engineering  Type Theory  2 comments  other blogs  6138 reads
Achieving 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  5557 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  11331 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  10540 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  13312 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  12701 reads

Browse archivesActive forum topics 
Recent comments
1 week 5 hours ago
1 week 1 day ago
1 week 1 day ago
2 weeks 4 days ago
2 weeks 4 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago