## User login## Navigation |
## Semantics## The Experimental Effectiveness of Mathematical ProofThe Experimental Effectiveness of Mathematical Proof
I thought I had already posted this, but apparently not. Consider this paper the main gauntlet thrown down to those who insist that mathematical logic, the Curry-Howard Isomorphism, etc. might be fine for "algorithmic code" (as if there were any other kind) but is somehow inapplicable the moment a system interacts with the "real" or "outside" world (as if software weren't real).
By Paul Snively at 2011-10-30 16:05 | Functional | Lambda Calculus | Logic/Declarative | Semantics | 32 comments | other blogs | 13466 reads
## A Semantic Model for Graphical User InterfacesNick Benton and Neel Krishnaswami, ICFP'11, A Semantic Model for Graphical User Interfaces:
This is an application of their (more squiggly) LICS'11 submission, Ultrametric Semantics of Reactive Programs. In both these cases, I find appealing the fact the semantic model led to a type system and a language that was tricky to find. By Ohad Kammar at 2011-09-10 20:25 | DSL | Fun | Functional | Paradigms | Semantics | Theory | 5 comments | other blogs | 14692 reads
## Lightweight Monadic Programming in MLLightweight Monadic Programming in ML
This is an intriguing paper, with an implementation in about 2,000 lines of OCaml. I'm especially interested in its application to probabilistic computing, yielding a result related to Kiselyov and Shan's Hansei effort, but without requiring delimited continuations (not that there's anything wrong with delimited continuations). On a theoretical level, it's nice to see such a compelling example of what can be done once types are freed from the shackle of "describing how bits are laid out in memory" (another such compelling example, IMHO, is type-directed partial evaluation, but that's literally another story). By Paul Snively at 2011-07-28 18:11 | Category Theory | Functional | Implementation | Semantics | Type Theory | 35 comments | other blogs | 21682 reads
## Levy: a Toy Call-by-Push-Value LanguageAndrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml. If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out. It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more hands-on way to get to grips with CBPV would be to implement any of these missing features. The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here. By Ohad Kammar at 2011-07-14 18:57 | Fun | Functional | Implementation | Lambda Calculus | Paradigms | Semantics | Teaching & Learning | Theory | 4 comments | other blogs | 31644 reads
## Imperative Programs as Proofs via Game SemanticsImperative Programs as Proofs via Game Semantics, Martin Churchill, James Laird and Guy McCusker. To appear at LICS 2011.
This paper increases the importance of gaining a more-than-casual understanding of game semantics for me, since it combines two of my favorite things: polarized type theories and imperative higher-order programs. ## Macros that Work TogetherMacros that Work Together - Compile-Time Bindings, Partial Expansion, and Definition Contexts, Matthew Flatt, Ryan Culpepper, David Darais, and Robert Bruce Findler. Under consideration for publication in J. Functional Programming.
A good description of Racket's rocket science tools for growing languages. By Manuel J. Simoni at 2011-02-03 14:25 | DSL | Meta-Programming | Semantics | login or register to post comments | other blogs | 10662 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. ## Abstract interpreters for free
The work in this paper provides some context for known static analysis techniques like By Allan McInnes at 2010-08-29 13:31 | Semantics | Teaching & Learning | 2 comments | other blogs | 8313 reads
## What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in CommonWhat Sequential Games, the Tychonoff Theorem, and the Double-Negation Shift have in Common, Martin Escardo and Paulo Oliva, to appear in MSFP 2010.
One of the most durable and productive analogies in semantics is the analogy between computability and continuity. Depending on how you read the history, this idea might even predate computers: Brouwer proved that all intuitonistic functions on the reals were continuous. Over the last few years, Escardo and his collaborators have done a lot of cool stuff showing how this network of ideas can be turned into miraculous-looking little programs, so it's very nice to see a relatively accesible introduction to this work. ## Handlers of Algebraic EffectsMatija Pretnar, Gordon Plotkin (2009) Handlers of Algebraic Effects:
Handling a computational effect, such as raising an exception, amounts to homomorphically mapping the handled computation onto another computation. So, for example, While encompassing both returning and non-returning handlers, this idea becomes more interesting when you start to handle the other effects, such as If you want a gentler introduction to the subject (along with Plotkin's algebraic theory of effects and Levy's Call-by-Push-Value), try Pretnar's 2010 thesis. |
## Browse archives## Active forum topics |

## Recent comments

3 days 14 hours ago

3 days 19 hours ago

3 days 21 hours ago

4 days 8 hours ago

6 days 3 hours ago

1 week 10 hours ago

1 week 10 hours ago

1 week 2 days ago

1 week 2 days ago

1 week 5 days ago