This is the homepage for CS 465: Language, Logic and Computation), a course offered by Fritz Ruehr at the Computer Science Department of Willamette University. The course develops formal languages from the perspectives of logic, mathematics and computer science, but emphasizes semantics of programs, in contrast with the traditional treatment of formal languages as sets of strings. It is organized as a tour of successively enriched object languages and of the meta-linguistic techniques needed to rigorously describe them.
The style of presentation will be influenced by functional programming, category theory, the Curry-Howard correspondence, and the Squiggol school of constructive programming (catamorphisms, anamorphisms, etc.); Haskell is used as an implementation meta-language.
The official course description reads:
Language is the basic for complex communication, whether as natural language between humans or as formal language between humans and computers. In programming, different kinds of formal languages are crucial tools in all stages of development, from the logics used to specify requirements, to the programming languages used to implement algorithms and the mathematical notations used to analyze their behavior. In this course we will study the general phenomenon of formal language by exploring the syntax, semantics and logics of a broad range of examples, beginning with the simplest numeral notations and operator algebras and continuing through to computationally complete languages and sophisticated type systems. In addition to studying abstract descriptions of syntax and semantics, students will reinforce their understanding by implementing language-based tools in a functional meta-language.
(This course is a rather idiosyncratic approach to a revised CS Theory curriculum; but the general topic is not without some precedent, as evidenced by, e.g., the Tbilisi Symposium on Language, Logic and Computation, the Institute for Logic, Language and Computation at Universiteit van Amsterdam (also here), the Journal of Language, Logic and Computation, the book Algebras, Diagrams and Decisions in Language, Logic and Computation, the breadth studies program in Language, Logic and Computation at The University of Melbourne, the Centre for Logic, Language and Computation at the University of Melbourne, the workshop Language, Logic, and Computation in Honor of Prof. Nachum Dershowitz, the The Association for Logic, Language and Information, and the Workshop on Logic, Language, Information and Computation, among others.)
Welcome to the 2015 version of the course!
We will be using the Haskell programming language as our primary meta-language and implementation vehicle. There are plenty of on-line resources on Haskell, how to use it, downloadable implementations, etc. For example, you can try Haskell out in your browser, including a nice set of guided lessons and exercises.
You might also want to take a look at a tutorial or two from this list at the Haskell Wiki pages. I especially recommend the book, available on-line for free, Learn You a Haskell for Great Good (complete with cartoons).
You also might want to download an implementation for use on your own machine; there is a fully-featured, multi-platform version available as the Haskell Platform; it includes an industrial-strength compiler and a bunch of libraries.
On the other hand, we really don‘t need all this power, so you might want to get the simpler Hugs system we use in the lab:
We won't be using a formal textbook this semester, so I will be trying to gather links to relevant on-line material. A lot of good-quality articles are available on Wikipedia, the free on-line "open source" encyclopedia.
We will need some basic background in set theory and related topics (orderings, functions, relations and some basic logic) as a foundation for later work. You should have some exposure to this material already, but I will work (quickly) through some review notes (to be linked above) in lecture. You can also read about some of the same topics at Wikipedia: