Update on the Software Languages Book

Deleting this post as it superseded by newer updates.

Comments

  1. UnknownSeptember 12, 2016 at 5:15 PM

    Interesting that you've removed all Prolog. I seem to be hearing about a lot of use of Datalog in program analysis circles: any thoughts on that?

    ReplyDelete
    Replies
    1. Ralf LämmelSeptember 12, 2016 at 7:00 PM

      Yes, Prolog and Datalog and DCG are great tools in metaprogramming. I just figured that I might get a bit more readers by more consistently relying on Haskell throughout. This nice side effect is that I now have many problems coded up both in Prolog and Haskell. Don't get anywhere interestingly deep into program analysis.

      Delete

Post a Comment

Popular posts from this blog

Lecture series on advanced (functional) programming concepts

[ Added 10 Aug 2010: Here is the link to the first lecture's video: " The Expression Problem ". ] If you are a programming nerd or something of a similar species, you may know of C9 Lectures at http://channel9.msdn.com/tags/C9+Lectures . Several of the lectures are given by Erik Meijer who has turned many chapters of Graham Hutton 's book " Programming in Haskell " into videos. In my recent, recorded lecture on " Programming Paradigms and Formal Semantics ", I also incorporated Graham's text, but you should really watch Erik's lectures, if you haven't---they are more fun. I am inspired by his ability to present relatively simple content in such a crisp, insightful, and enjoyable manner. In the aforementioned lecture, I covered all kinds of "crazy stuff" though, and in the end, I had to deliver body bags to my Bachelor students---in the form of a radically simple examination. Thanks a lot btw to @grammarware for helping with t...
Read more

Vorlesung kämpft um ihre Austragung

Durch eine Vollversammlung der Studenten wurde heute auf dem Campus beschlossen, dass unser, über alles geliebte AUDIMAX (grosser Hörsaal D 028) besetzt wird. Dies zu tun, ist das demokratische Recht der Studenten und deren Argumentation ist anderswo verfügbar. Ich werde mich hier dazu nicht weiter äussern. Allerdings überlege ich gerade, ob und wie diese Aktion meine donnerstägliche OOPM- Vorlesung in eben diesem Raum (follow @oopm, siehe Link hier http://userpages.uni-koblenz.de/~laemmel/oopm0910/ ) beeinträchtigt. Da weder AStA noch die Uni-Leitung, noch irgend jemand anders mit Autorität, so weit ich weiss, bisher klare Empfehlungen gibt, was anstehende Veranstaltungen im D 028 angeht, versuche ich mal etwas OOPM-spezifisches -- in der Hoffnung dass ich nicht unwissentlich meine Beamten- und demokratischen Pflichten verletze: Gelingen und Kooperation durch die Besatzungsmacht vorausgesetzt, findet die morgige OOPM-Veranstaltung im D 028 in unkonventionellerer Form statt. Ich höre...
Read more

A tiny proof checker in Prolog

The Prolog code for this post is available on GitHub . I am crazy enough to teach Hoare logic (axiomatic semantics) in the first course for our CS students. For instance, consider the following program (in some simple imperative language), which is supposed to compute quotient q and remainder r according to Euclidian division for operands  x and y : q = 0; r = x; while (r >= y) { r = r - y; q = q + 1; } Given natural numbers x and y , the postcondition of the program is this: x == q*y + r && q >= 0 && r>=0 && r < y The precondition is this is: x >= 0 && y > 0 We are supposed to prove the "triple" consisting of precondition, program, and postcondition. Let's face it, verification according to Hoare logic is not easily understood by beginners. Many of my students aren't mathematically / logically fit, when they enter the curriculum. So it is a pain in the neck for them to listen and for ...
Read more