tag:blogger.com,1999:blog-7916186343546411062018-09-17T09:45:18.749+01:00Why $\lambda$‽A research blog about programming languages, databases, provenance, and other randomly-selected topics.James Cheneynoreply@blogger.comBlogger47125tag:blogger.com,1999:blog-791618634354641106.post-35127068844392706132018-08-12T18:23:00.000+01:002018-08-12T18:24:20.411+01:00Recursion in RI've been (trying to) learn a little about R, mostly in self-defense because I'm involved in a project with others using it.<br><br>R has lots of fun features, such as built-in support for vector and matrix operations and overloading, which make it well-suited to its domain, statistical programming and modeling.<br><br>However, there are also some things that are just plain weird, at least from the point of view of programming language design. Scoping and lazy evaluation interact in a subtle way, particularly with regard to recursion.<br><br><a href="http://why-lambda.blogspot.com/2018/08/recursion-in-r.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-30491189504840375312017-12-13T15:55:00.001+00:002017-12-13T15:58:12.942+00:00Defining backticks using "pipe" operations(Thanks to Simon Fowler and others on the <a href="http://links-lang.org/">Links</a> team for the discussion leading to this...)<br><br>In Haskell, you can use a 2-argument function as if it were an infix operator by putting "backticks" around it like this:<br><br><span style="font-family: "courier new" , "courier" , monospace;">ghci> let plus x y = x + y</span><br><span style="font-family: "courier new" , "courier" , monospace;">ghci> 1 `plus` 2</span><br><span style="font-family: "courier new" , "courier" , monospace;"><i>3</i> </span><br><br>In a number of functional languages such as F# and OCaml, the following "pipe" operations have become popular (I'll continue using Haskell syntax, though):<br><br><span style="font-family: "courier new" , "courier" , monospace;">ghci> let (|>) x f = f x</span><br><span style="font-family: "courier new" , "courier" , monospace;">ghci> let (<|) f x = f x</span><br><span style="font-family: "courier new" , "courier" , monospace;">ghci> [1,2,3] |> map (plus 1)</span><br><span style="font-family: "courier new" , "courier" , monospace;"><i>[2,3,4] </i></span><br><br><br><a href="http://why-lambda.blogspot.com/2017/12/defining-backticks-using-pipe-operations.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com3tag:blogger.com,1999:blog-791618634354641106.post-46517183198515898572016-04-28T11:36:00.003+01:002016-04-28T11:37:04.756+01:00Summer school on bidirectional transformationsLady Margaret Hall, Oxford, UK<br>25th to 29th July 2016<br>http://www.cs.ox.ac.uk/projects/tlcbx/ssbx/<br><br><h3>TOPIC</h3><br>Bidirectional transformations (BX) are means of maintaining consistency between multiple information sources: when one source is edited, the others may need updating to restore consistency. BX have applications in databases, user interface design, model-driven development, and many other domains. This summer school is one of the closing activities on the "<a href="http://www.cs.ox.ac.uk/projects/tlcbx/">Theory of Least Change for BX</a>" project at Oxford and Edinburgh. It brings together leading researchers in BX, spanning theory and<br>practice, for a week of lectures in beautiful Oxford. It will be aimed at doctoral students in computer science, but will also be suitable for strong master's students and for researchers.<br><br><a href="http://why-lambda.blogspot.com/2016/04/summer-school-on-bidirectional.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-71762824519758821662016-03-01T17:14:00.002+00:002016-03-01T17:15:43.133+00:00PhD studentships in programming languages, provenance, data managementI am currently advertising two PhD studentships, on topics spanning programming languages, provenance, and data management, to start in fall 2016. <br><br>Both of these studentships are fully funded for applicants of any nationality (in contrast to many UK PhD studentships which are only funded up to the UK/EU tuition level, and do not cover full tuition fees for students from outside the European Union.) <br><a href="http://why-lambda.blogspot.com/2016/03/phd-studentships-in-programming.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-39455349120280932492016-01-13T10:32:00.002+00:002016-01-13T10:32:49.828+00:00Reflections on monadic lensesThanks to Matt Might for some very kind words on our paper "<a href="http://arxiv.org/abs/1601.02484">Reflections on monadic lenses</a>", recently posted to arXiv.org and scheduled to appear in April as part of an upcoming <a href="http://events.inf.ed.ac.uk/wf2016/">Festschrift for Phil Wadler</a>.<br /><br /><blockquote class="twitter-tweet" lang="en"><p lang="en" dir="ltr">A great review of bidirectional programming with (monadic) effects: <a href="https://t.co/rea2JJcTnX">https://t.co/rea2JJcTnX</a> by <a href="https://twitter.com/jer_gib">@jer_gib</a> & co.</p>— Matt Might (@mattmight) <a href="https://twitter.com/mattmight/status/686972298641944576">January 12, 2016</a></blockquote><script async src="//platform.twitter.com/widgets.js" charset="utf-8"></script>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-59481106283256979882015-11-05T11:43:00.001+00:002015-11-22T20:56:07.962+00:00Private type members in Scala aren't I haven't posted in a while now, and one major reason is that I've been teaching a new <a href="http://www.inf.ed.ac.uk/teaching/courses/epl/">course on Programming Languages</a>. I've been using Scala, somewhat experimentally, and as a (perhaps misguided) way of forcing myself to learn some Scala.<br><br>In the last few lectures, I've been covering Scala's object system. I'm not an expert on Scala by any means, but I was a little surprised by the way "private" appears to work (or more accurately, not work) on type members of classes/objects.<br><br><a href="http://why-lambda.blogspot.com/2015/11/private-type-members-in-scala-arent.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com3tag:blogger.com,1999:blog-791618634354641106.post-42248554337909364892015-07-24T16:42:00.002+01:002015-07-24T16:43:07.624+01:00Call for participation: DBPL 2015<b>The 15th International Symposium on Database Programming Languages</b><br><a href="http://2015.splashcon.org/track/dbpl2015">http://2015.splashcon.org/track/dbpl2015</a><br>Pittsburgh, Pennsylvania, USA<br>October 27, 2015<br>hosted as part of <a href="http://2015.splashcon.org/">SPLASH 2015</a><br><br><h2>Call for Participation</h2>DBPL has a long tradition of bringing databases and programming languages together. This year we continue this tradition by co-locating DBPL with SPLASH 2015, and presenting an interesting mix of papers with programming language and database aspects. In addition to these papers we have an excellent invited talk by Marko Rodriguez of DataStax about Gremlin: A Stream-Based Functional Language for OLTP and OLAP Graph Computing. We hope to see you in Pittsburgh!<br><br>DBPL is held in cooperation with ACM SIGPLAN, and gratefully acknowledges support from LogicBlox, Inc.<br><br><a href="http://why-lambda.blogspot.com/2015/07/call-for-participation-dbpl-2015.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-58882358359105534042015-04-14T16:00:00.000+01:002015-05-12T12:14:41.880+01:00Mechanized formalizations of the pi-calculus (and friends)I recently started to put together a bibliography (as complete as I can make it) of mechanized formalizations of the pi-calculus (and close relations). I also asked for additional suggestions on the TYPES mailing list, and received several helpful responses. Here is the complete list, as of today.<br><br>I hope to use this as a starting point to understand the strengths and weaknesses of different approaches (and any gaps in the literature) but so far I have not read most of these papers. Nevertheless I am posting this without any further discussion in case it is helpful to anyone else interested in this topic in the future.<br><br>Thanks to Robert Harper, Dale Miller, Dominic Orchard, Francois Pottier, Ivan Scagnetto, Gabriel Scherer, and Tjark Weber for their suggestions.<br><br>[<b>Updated: </b>Thanks also to Tobias Nipkow and Jeremy Siek for spotting some typos and misclassifications, and Alan Schmitt for a link to more information on HOCore.]<br><br>[<b>Updated 2:</b> to include Christine Rockl's MERLIN 2001 paper on a formalization of the pi-calculus in Isabelle/HOL using Gabbay-Pitts permutation-based syntax.]<br><br>[<b>Updated 3:</b> to include more recent work on formalising psi-calculi using Nominal Isabelle.] <br><a href="http://why-lambda.blogspot.com/2015/04/mechanized-formalizations-of-pi.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com4tag:blogger.com,1999:blog-791618634354641106.post-86323080873807615672015-01-14T11:10:00.000+00:002015-07-24T16:47:19.922+01:00How to publish research accompanied by mechanically-checkable proofsI've both written and reviewed research papers that incorporate mechanically-checked proofs (either as the main subject of the research or as supporting the correctness of other contributions). Computer-aided formalization and proof are increasingly part of the mainstream of (the formal side of) programming languages research, and seem to be being especially enthusiastically adopted by students and junior researchers. However, just having mechanically verified a proof of (some aspect of) a system is <b>not enough</b> - all of the standard considerations regarding the reporting of scientific research, on-paper proofs, or research code still apply. <br><br>This post collects some guidelines that I hope will be helpful for researchers working on papers accompanied by formal proofs. I would have thought most of these were obvious, but have encountered enough counterexamples to disabuse me of this naive assumption. The following is probably not an exhaustive list, but is offered as a starting point.<br><br><br><a href="http://why-lambda.blogspot.com/2015/01/how-to-publish-research-accompanied-by.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com2tag:blogger.com,1999:blog-791618634354641106.post-35267989272458340332014-11-11T11:32:00.000+00:002014-11-11T11:32:06.642+00:00PhD and Postdoctoral Positions<a href="http://homepages.inf.ed.ac.uk/jcheney/lbps.html"><b>PhD and Postdoctoral Positions in Language-based Provenance Security</b></a><br /><br /><b> </b><br />We seek strong candidates for <br /><ul><li> a PhD studentship (covering full stipend and tuition for a student of any nationality for three years) </li><li>a postdoctoral researcher (for 12 months, with possibility of renewal) </li></ul>on the topic of foundations of language-based provenance security. Funding is provided by a four-year research grant provided by the AFOSR European Office of Aerospace Research and Development. <br />The PhD student and postdoctoral researcher working on this project will play an important role in one or more of the following project tasks: <br /><ul><li>Enrich and extend formal models of provenance from simple programming languages or database query languages to handle features such as concurrency, references, side-effects, notions of location, time, or boundaries of control</li><li>Analyze existing proposals for provenance security mechanisms, and identify shortcomings or generalizations leading to a richer understanding of policies and correct mechanisms for provenance</li><li>Develop efficient techniques for integrating provenance-tracking techniques into programming languages or other frameworks</li><li>Formalize and verify provenance techniques in mechanized proof systems or dependently-typed languages such as Coq, Agda or Isabelle/HOL </li></ul><b>Deadlines:</b><br /><br />Postdoctoral position: November 24, 2014.<br />PhD studentship: December 12, 2014. <br /><br /><a href="http://homepages.inf.ed.ac.uk/jcheney/lbps.html">More information here</a><b> </b><br /><br />James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-48070244429635351572014-09-30T18:46:00.005+01:002015-07-23T15:08:23.584+01:00Dijkstra monads<a href="http://www.cs.ru.nl/B.Jacobs/PAPERS/Dijkstra-monad.pdf">Dijkstra monads in monadic computation</a><br>Bart Jacobs<br>CMCS 2014<br><br>This paper discusses a monad for predicate transformers (dubbed the Dijkstra monad in an earlier paper by <a href="http://doi.acm.org/10.1145/2491956.2491978">Swamy et al.</a> that is now also on my reading list). This post is an attempt to express a very, very small part of the ideas of the paper in Haskell, to try to make some sense of them.<br><br><a href="http://why-lambda.blogspot.com/2014/09/dijkstra-monads.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com8tag:blogger.com,1999:blog-791618634354641106.post-73209991762338939512014-09-29T15:53:00.001+01:002014-09-29T15:53:47.501+01:00PPDP 2014PPDP 2014<br><br>I attended PPDP 2014, in Canterbury, England a few weeks ago. Some notes about papers of interest there:<br><br><br><a href="http://why-lambda.blogspot.com/2014/09/ppdp-2014.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-59522046327533279702014-09-12T18:24:00.000+01:002014-09-12T18:24:37.406+01:00F# London meetup - FSharpComposableQuery demo<a href="http://www.meetup.com/FSharpLondon/">F#unctional Londoners meetup - FSharpComposableQuery demo</a><br /><br />I volunteered to give a talk/demo at the F# London meetup <a href="http://www.meetup.com/FSharpLondon/events/201525352/">yesterday evening</a> which meets at the <a href="https://skillsmatter.com/locations/96-skills-matter-exchange">Skills Matter Exchange</a>. I gave a high-level overview of what we have been doing with <a href="http://fsprojects.github.io/FSharp.Linq.ComposableQuery/">FSharpComposableQuery</a>. The slides and demo code I used are available <a href="http://homepages.inf.ed.ac.uk/jcheney/linq/index.html#meetup">here</a>, and there is a video <a href="https://skillsmatter.com/locations/96-skills-matter-exchange">here</a>. I haven't watched the whole thing and am not sure how comprehensible it (or I) am; I get that weird feeling because my voice sounds different than I think it should and can't watch it very long. YMMV.<br /><br />The talk seemed to go over well, and there were 30-40 people. It was a very friendly atmosphere and I talked afterwards with several people that are familiar with settings where what we have been doing would be useful, so I'm hoping we'll get some feedback from anyone willing to try it out.James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-56350796673530720222014-08-29T17:07:00.004+01:002014-08-29T17:07:48.037+01:00Summer readingFor various reasons I haven't had time to make even semi-regular blog posts, so I thought I'd clear the decks a little by listing selected contents of my "recently read" basket, before I file them.<br><br><br><a href="http://why-lambda.blogspot.com/2014/08/summer-reading.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-2682911765508363942014-08-04T12:16:00.004+01:002014-08-04T12:18:57.826+01:00More on composing queries in F#I ran across some StackOverflow questions from a couple of years ago asking about composing query expressions in F#, and gave answers showing how <span style="font-family: "Courier New",Courier,monospace;">FSharpComposableQuery</span> can help with this:<br><br>http://stackoverflow.com/questions/13826749/how-do-you-compose-query-expressions-in-f<br><br>http://stackoverflow.com/questions/10158512/dynamic-sql-queries-with-f-3-0<br><br>Tomas Petricek's previous posts on <a href="http://tomasp.net/blog/dynamic-linq-queries.aspx">dynamic LINQ queries in C#</a> and <a href="http://tomasp.net/articles/dynamic-flinq.aspx">F# 2.0</a> were, of course part of the inspiration for our work. <span style="font-family: "Courier New",Courier,monospace;">FSharpComposableQuery</span> updates these ideas to F# 3.0 and, hopefully, makes them easily usable without the need for tricks.<br><br>I also ran across a <a href="http://fpish.net/blog/loic.denuziere/id/3508/2013924-f-query-expressions-and-composability">more recent blog post by Loïc Denuziere</a> that discusses the related issue of how to splice partial F# query expressions together to build more complex ones. His approach cleverly defines an alternative query operator, <span style="font-family: "Courier New", Courier, monospace;">pquery</span>, that can be used to define query snippets that don't get evaluated immediately. He suggests the following code (copied from the end of the post):<br><br><a href="http://why-lambda.blogspot.com/2014/08/more-on-composing-queries-in-f.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-29353366144220974242014-07-28T14:44:00.003+01:002014-08-01T15:21:40.040+01:00Composing queries in F#<br>In our <a href="http://dl.acm.org/citation.cfm?doid=2500365.2500586">ICFP 2013</a> paper last year, we introduced a formal model of Microsoft's "Language-Integrated Query", as implemented in F#. The basic idea is to allow programmers to write queries in a way that more closely resembles ordinary code, can be typechecked alongside ordinary code, but still (hopefully) generates reasonable SQL queries. For example, in F# one can write something like<br><br><br><pre class="fssnip"><span style="font-family: "Courier New",Courier,monospace; font-size: small;">query {<br> for student in db.Student do<br> where (student.Age.Value >= 10 <br> && student.Age.Value < 15)<br> select student<br> }</span></pre><br>to select all students with ages in the interval $[10,15)$.<br><br>Observe that the above query does not depend on any data in the F# host language. There's a single SQL query that we can generate to answer this query on the database:<br><pre><span style="font-family: "Courier New",Courier,monospace;"><br>SELECT student<br>FROM Student student<br>WHERE student.Age >= 10 AND student.Age < 15</span></pre><br><br>(here, I'm glossing over differences in SQL syntax between Microsoft SQL server and other DBMSs).<br><br><a href="http://why-lambda.blogspot.com/2014/07/composing-queries-in-f.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-78772044890190747122014-06-27T01:52:00.000+01:002018-08-12T18:38:04.353+01:00SIGMOD 2014I totally failed to post a trip report on POPL 2014, and I'm now attending <a href="http://www.sigmod2014.org/">SIGMOD/PODS 2014</a>, in Snowbird, Utah, so I'm writing the post during the conference to ensure I don't forget later. This is the first time I've been to SIGMOD in a while. There are usually 4-5 parallel tracks so it is impossible to see more than a fraction of the talks, but fortunately the talks I was most interested in were usually in separate sessions, so there were only a few tough decisions. There were many good talks, but several stood out:<br><a href="http://why-lambda.blogspot.com/2014/06/sigmod-2014.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-24036636818376353042014-05-01T13:10:00.002+01:002014-05-01T13:12:02.821+01:00Observing SQL queries in their natural habitatTorsten Grust and Jan Rittinger. 2013. <a href="http://doi.acm.org/10.1145/2445583.2445586">Observing SQL queries in their natural habitat</a>. <i>ACM Trans. Database Syst.</i> 38, 1, Article 3 (April 2013), 33 pages.<br><br>This paper presents a system called Habitat, that allows highlighting a subexpression of an SQL query whose results are of interest (e.g. due to surprising/incorrect query results). The system then compiles it into another query whose results are rows containing the values of variables in the "closure" (that is, the values of variables bound outside the subexpression) and the associated values of the selected query.<br><br><a href="http://why-lambda.blogspot.com/2014/05/observing-sql-queries-in-their-natural.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-924718876840513242014-04-14T17:35:00.003+01:002014-06-27T01:54:43.138+01:00Two reversible forms of CCSDanos, V. and Krivine, J., <a href="http://link.springer.com/chapter/10.1007%2F978-3-540-28644-8_19">Reversible communicating systems</a>. CONCUR 2004, LNCS, 3170. pp. 292-307.<br><br>Iain C. C. Phillips, Irek Ulidowski: <a href="http://dx.doi.org/10.1016/j.jlap.2006.11.002">Reversing algebraic process calculi</a>. J. Log. Algebr. Program. 73(1-2): 70-96 (2007) <br><br>These two papers present different views on reversibility for CCS. In both cases, a key question is how to deal with a process term such as $(a.P | a.Q | \bar{a}.R| \bar{a}.S) \backslash a$ which can evolve in two different ways, both leading to the same state $(P|Q|R|S)$: one where the $a.P$ and $\bar{a}.R$ synchronize, and one where $a.P$ and $\bar{a}.S$ synchronize. A key question is, what additional information do we need to record so that the right synchronizations are undone.<br><br><a href="http://why-lambda.blogspot.com/2014/04/two-reversible-forms-of-ccs.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-65640629962863776442014-04-07T18:40:00.002+01:002014-06-27T01:54:28.851+01:00PhD studentship in data-centric programming at LFCS, University of Edinburgh<br>A fully-funded 3-year PhD studentship has become available in LFCS in data-centric programming. Applications and expressions of interest are welcome now, with a closing date of April 28, 2014.<br><br>This studentship is partly funded by a EU FP7 project (DIACHRON) and partly by a Google Research Award. The funding includes UK/EU tuition and fees, and a non-taxable stipend of approximately £13,800 per year for 3 years; a small amount of additional funding is available that may be used flexibly for equipment, travel or additional stipend support. <br><br><a href="http://why-lambda.blogspot.com/2014/04/phd-studentship-in-data-centric.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-69673213813267218802014-03-21T17:20:00.003+00:002014-06-27T01:55:09.989+01:00Reproducibility and information preservation<a href="http://reproducibility.cs.arizona.edu/tr.pdf">Measuring reproducibility in computer systems research</a><br><br><div class="page" title="Page 1"><div class="layoutArea"><div class="column"><span style="font-family: 'CMR12'; font-size: 12.000000pt;">Christian Collberg, Todd Proebsting, Gina Moraila, Akash Shankara, Zuoming Shi and Alex M Warren </span></div></div></div><br>The reproducibility, or lack thereof, of scientific research is a hot topic recently. Among real scientists, reproducibility of experiments has always been an important goal, although as experimental materials and volumes of data they can generate have grown rapidly, it is becoming more and more difficult to achieve this goal. In principle, the "Methods and Materials" section of a scientific journal article should provide the information needed (at least, for another qualified scientist in the same area) to reproduce the results. In practice, this is not always possible, although one must at least pay lip service to this in order to get a paper accepted. In some domains, however, it is estimated that up to <a href="http://www.nature.com/news/nih-mulls-rules-for-validating-key-results-1.13469">half or more of reported results are irreproducible</a>; however, once a result is published (especially by a high-profile journal) it can become difficult for others to publish results that contradict apparently-established facts.<br><br><a href="http://why-lambda.blogspot.com/2014/03/reproducibility-and-information.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-61251226543392327722014-03-16T15:25:00.000+00:002014-03-16T15:29:47.872+00:00Introduction to Bisimulation and CoinductionIntroduction to Bisimulation and Coinduction<br>Davide Sangorgi<br>Cambridge University Press, 2012<br><br>Bisimulation is a natural notion of equivalence for process algebras, and arises naturally in modal logic, graph theory and other settings. Suppose we have a labeled transition system $(X,\stackrel{a}{\to})$, then a bisimulation $R$ is a relation satisfying:<br><br><ul><li>for all $x~R~y$, if $x \stackrel{a}{\to} x'$ then there exists $y'$ such that $y \stackrel{a}{\to} y'$</li><li>for all $x~R~y$, if $y \stackrel{a}{\to} y'$ then there exists $x'$ such that $x \stackrel{a}{\to} x'$</li></ul>Then bisimilarity is defined as the largest relation $\approx$ that contains every bisimulation. Equivalently, the largest relation closed under the above two rules.<br><br>Bisimulation is defined <i>coinductively,</i> that is, in terms of the greatest fixed point of a monotone operator, in contrast to inductive definitions (least fixed-points) that are more familiar to computer scientists. Bisimulation and coinduction are general concepts, but they have generally been covered in the context of process calculi such as CCS or the $\pi$-calculus, or for reasoning about infinite streams or other infinite behaviors in functional programming. This book provides an accessible treatment of both topics in their own right, rather than as a secondary matter arising in the study of process calculus or streams. <br><a href="http://why-lambda.blogspot.com/2014/03/introduction-to-bisimulation-and.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-25564724393048385792014-03-07T15:46:00.001+00:002014-03-16T15:26:09.894+00:00Programming with Higher-Order Logic<a href="https://sites.google.com/site/proghol/">Programming with Higher-Order Logic</a><br>Dale Miller and Gopalan Nadathur<br>Cambridge University Press 2013<br><br>Church's higher-order logic, based on the typed $\lambda$-calculus, is a foundation of mathematics and computer science. It underpins a number of other influential logics and type theories, including systems for formalized mathematics such as LF, HOL and Coq, which in turn have led to interesting developments relevant to mainstream mathematics such as formal proofs of the Four-Color Theorem and Feit-Thompson Theorem in Coq, as well as the Homotopy Type Theory program initiated by Voevodsky. This book is about higher-order logic viewed in a different light, as a foundation for programming, specifically following the <i>computation-as-deduction</i> approach taken in logic programming languages such as Prolog. Higher-order logic programming builds on higher-order unification, and generalizes Horn clauses over first-order terms in Prolog to hereditary Harrop formulas over higher-order terms in languages such as $\lambda$Prolog. One might view (higher-order) logic programming as a tool deserving a place in a logician's toolbox analogous to numerical or symbolic tools for analysis: not a replacement for mathematical reasoning, but a framework for experimentation and automation. <br><br><a href="http://why-lambda.blogspot.com/2014/03/programming-with-higher-order-logic.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-8262480361408075322013-12-19T17:13:00.001+00:002013-12-19T17:15:07.033+00:00Asynchronous functional reactive programming for GUIs<a href="http://dx.doi.org/10.1145/2499370.2462161">Asynchronous functional reactive programming for GUIs</a><br>Evan Czaplicki and Stephen Chong<br>PLDI 2013 (see also http://elm-lang.org/)<br><br>This paper presents a new functional reactive programming-based programming language aimed at graphical user interaction (particularly on Web pages as embedded in Javascript). Graphical user interaction has frequently been cited as a motivation for FRP techniques since the first work on it by <a href="http://conal.net/papers/icfp97/">Elliott and Hudak</a>. Early techniques had some significant performance problems, while more recent techniques have introduced restrictions or refinements that seek to reconcile convenient programming with efficiency.<br><br><a href="http://why-lambda.blogspot.com/2013/12/asynchronous-functional-reactive.html#more">Read more »</a>James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0tag:blogger.com,1999:blog-791618634354641106.post-2802775284068472702013-12-17T12:00:00.003+00:002013-12-19T17:14:29.327+00:00InterrobangI'm trying out an <a href="http://www.shadycharacters.co.uk/2011/04/the-interrobang-part-1/">interrobang</a> (‽) in the blog title. I'll give it a few days to see how it looks.<br /><br />(Update: Think I'll keep it.) James Cheneyhttps://plus.google.com/112386559365297096859noreply@blogger.com0