User loginNavigation 
Logic/DeclarativeExtensible Effects  An Alternative to Monad TransformersExtensible Effects  An Alternative to Monad Transformers, by Oleg Kiselyov, Amr Sabry and Cameron Swords:
A followup to Oleg's delimited continuation adaptation of Cartwright and Felleisen's work on Extensible Denotational Language Specifications, which is a promising alternative means of composing effects to the standard monad transformers. This work embeds a userextensible effect EDSL in Haskell by encoding all effects into a single effect monad using a novel open union type and the continuation monad. The encoding is very similar to recent work on Algebraic Effects and Handlers, and closely resembles a typed clientserver interaction ala coroutines. This seems like a nice convergence of the topics covered in the algebraic effects thread and other recent work on effects, and it's more efficient than monad transformers to boot. By naasking at 20130729 14:53  Functional  Logic/Declarative  Theory  Type Theory  22 comments  other blogs  26254 reads
Visi.ioVisi.io comes from David Pollak and aims at revolutionizing building tablet apps, but the main attraction now seems to be in exploring the way data flow and cloud computing can be integrated. The screencast is somewhat underwhelming but at least convinces me that there is a working prototype (I haven't looked further than the website as yet). The vision document has some nice ideas. Visi.io came up recently in the discussion of the future of spreadsheets. By Ehud Lamm at 20121027 09:36  Functional  Logic/Declarative  Parallel/Distributed  2 comments  other blogs  11366 reads
How to Make Ad Hoc Proof Automation Less Ad HocHow to Make Ad Hoc Proof Automation Less Ad Hoc
If you've ever toyed with Coq but run into the difficulties that many encounter in trying to construct robust, comprehensible proof scripts using tactics, which manipulate the proof state and can leave you with the "ground" of the proof rather than the "figure," if you will, in addition to being fragile in the face of change, you may wish to give this a read. It frankly never would have occurred to me to try to turn Ltac scripts into lemmas at all. This is much more appealing than most other approaches to the subject I've seen. By Paul Snively at 20120622 15:41  Functional  Implementation  Logic/Declarative  Type Theory  9 comments  other blogs  7853 reads
Interactive Tutorial of the Sequent CalculusInteractive Tutorial of the Sequent Calculus by Edward Z. Yang.
The tool behind this nice tutorial is Logitext. By Manuel J. Simoni at 20120531 14:48  Fun  Javascript  Logic/Declarative  Teaching & Learning  Theory  28 comments  other blogs  12757 reads
Milawa on Jitawa: a Verified Theorem Prover
This is pretty interesting: Milawa was already "selfverifying," in the sense explained on the page. More recently, it's been made to run on a verified Lisp runtime, so that means the entire stack down to the X86_64 machine code is verified. Milawa itself is "ACL2like," so it's not as interesting logically as, say, Isabelle or Coq, but it's far from a toy. Also, the Jitawa formalization apparently took place in HOL4, so you need to trust HOL4. Since HOL4 is an "LCFlike" system, you can do that to the extent that you trust the LCF process, but it doesn't satisfy the de Bruijn criterion in the same way Milawa or Coq do. Nevertheless, this seems like an important step toward the ultimate goal of having a stack that is verified "all the way down," as it were. By Paul Snively at 20120229 18:34  Functional  Lambda Calculus  Logic/Declarative  2 comments  other blogs  6958 reads
Beyond pure Prolog: Power and dangerOne of the sections of Oleg Kiselyov's Prolog and Logic Programming page, on Beyond pure Prolog: power and danger, points out (i) term introspection (in the guise of the Oleg pointed this note in response to my defence of cut; it is short, sweet, and wellargued. By Charles Stewart at 20120123 10:54  Logic/Declarative  login or register to post comments  other blogs  8211 reads
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 CurryHoward 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). Update: the author is Alexandre Miquel, and the citation is "Chapitre du livre Anachronismes logiques, Ã paraÃ®tre dans la collection Logique, Langage, Sciences, Philosophie, aux Publications de la Sorbonne. Ã‰d.: Myriam Quatrini et Samuel TronÃ§on, 2010." By Paul Snively at 20111030 16:05  Functional  Lambda Calculus  Logic/Declarative  Semantics  32 comments  other blogs  11578 reads
Concurrent Pattern CalculusConcurrent Pattern Calculus by Thomas GivenWilson, Daniele Gorla, and Barry Jay:
Barry Jay's Pattern Calculus has been discussed a few times here before. I've always been impressed with the pattern calculus' expressive power for computing over arbitrary structure. The pattern calculus supports new forms of polymorphism, which he termed "path polymorphism" and "pattern polymorphism", which are difficult to provide in other calculi. The closest I can think of would be a compilerprovided generalized fold over any userdefined structure. This work extends the pattern calculus to the concurrent setting by adding constructs for parallel composition, name restriction and replication, and argues convincingly for its greater expressiveness as compared to other concurrent calculi. He addresses some of the obvious concerns for symmetric information flow of the unification operation. By naasking at 20110125 03:19  Functional  Logic/Declarative  Parallel/Distributed  Theory  1 comment  other blogs  7281 reads
Milawa: A SelfVerifying Theorem Prover for an ACL2Like LogicMilawa: A SelfVerifying Theorem Prover for an ACL2Like Logic
This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview. By Paul Snively at 20100529 17:49  DSL  Functional  Implementation  Lambda Calculus  Logic/Declarative  Semantics  11 comments  other blogs  9480 reads
A Lambda Calculus for Real AnalysisA Lambda Calculus for Real Analysis
Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated JeanYves Girard's regrettably outofprint Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX. By Paul Snively at 20100216 22:00  Category Theory  Functional  Lambda Calculus  Logic/Declarative  MetaProgramming  Semantics  Type Theory  9 comments  other blogs  11538 reads

Browse archives
Active forum topics 
Recent comments
1 hour 6 min ago
1 hour 9 min ago
1 hour 17 min ago
1 hour 21 min ago
1 hour 23 min ago
1 hour 44 min ago
1 hour 51 min ago
1 hour 52 min ago
2 hours 11 min ago
2 hours 34 min ago