About the course
This is the homepage for
CS 465: Language, Logic and Computation),
a course offered by
Fritz Ruehr at the
Computer Science Department of
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
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
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!
- Study for the final exam using
these final exam review notes.
... and check out this list of skills.
- Here is the promised paper on the phenomenon of reflection in various
systems, including biology (DNA and protein structure), linguistics, and
lambda calculus (see esp. pages 1-10):
Reflection and its Use
by Henk Barendregt.
short description of type systems
some inference rules for a typed calculus.
- The new homework assignment on lambda calculus and combinators is
- Some links on combinators (variable-free theory of functions):
- Here are some outline-formatted notes on lambda calculus (study-guide style):
notes on lambda calculus.
- Some materials on lambda calculus:
- Just for fun:
The Mathematician‘s Alphabet
- You can find the new homework assignment on formal proofs
- According to this article in the research journal of the
British Psychological Society, we
think more rationally in a non-native language.
this must have implications for the psychology of formal languages.
- The midterm grades are summarized in
- Some materials on logic:
- Here are some presentations of deduction rules:
- Here is a
sample deduction or two.
- Here are some links at Wikipedia relevant to logic:
- Once we’re done with the midterm, we will take a look at this
application of “folds-as-compositional-semantics” to
print out full truth tables (which would have been helpful for
doing and grading homework and exam problems):
- Lab 2 on parsing Java
is now available. The Haskell code file you will use in this
(See also the monadic parsing resources listed below.)
- The midterm is still being graded; hopefully
it will turn out better than
the 2011 midterm.
- Some materials on monadic parser combinators:
- For Friday, March 6, we’ll clean up loose ends on semantics
for algebraic terms, including polynomial function semantics and
propositional logic; see these files:
(Perhaps we should also consider porpositional logic,
which concerns reasoning about the location of dolphins … .)
- For Monday, March 2, we’ll be working on terms with variables
and (polynomial) function semantics, using this file:
- Some links for lecture (Wed 25 Feb):
- Regarding algebraic terms, see
this diagram and
(Plus, see this diagram re last lecture.)
- Get the latest lecture/outline
- Some links for lecture, Wed 18 Feb 2015:
- Here is a
quick summary of regular language definitions,
including REs, DFAs, and NFAs.
- Lab 1 on regular languages
is now available. The Haskell code file you will use
(i.e., read, digest, experiment with, and extend) is
available in two versions (text and PDF) as:
- Here are the
hints about the state-ripping transformation
from NFAs to REs.
- (I made a quick update to
the topical calendar
to reflect our current routing through
the basic math and language materials.)
- Slight (or is it “sleight”?) change of plans: we will
move right from [Symbols, strings, and sequences] to [Regular languages],
topically speaking. You can find a broad summary “road map”
of the various concepts and constructions involved here:
regular languages roadmap.
- You can read the details of the UTF-8 encoding scheme for Unicode characters at
Wikipedia page on UTF-8;
you might pay special attention to the
and the “salient features” bullet list that follows. Since the encoding
is pretty straightforward, but also technically adept (and cute/slick), I will
include it amongst the skills I allow myself to test on exams.
- Here are some course-wide documents, for posterity & reference:
- The little mini-lab for students who have just been introduced to Haskell
is now available as
Lab Zero. This lab will not be graded,
but rather gone over in lab: it is intended to helo those who need it
get started with Haskell (or get back “get back in the saddle”
if they’ve been away from it for a while).
- [Quick political aside: You just can’t buy irony this good;
I opened the news this morning to find these 2 articles listed one
right after the other:
I guess I should be glad to live in a time when entertainment is so cheap!]
Laurie Penny on the Eton scholarship question;
NYPD to patrol protests with machine guns.
- Here are links to diagrams about:
- The review of math is available,
although not complete (as of Wed 21 Jan); more to come soon!
- Here are the “chunking” exercises for those who are new to Haskell.
Labs (in rev. chron. order)
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
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:
Some topical references
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"
- Math review
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:
- Sets, domains and types
- Some references on symbols (Unicode and semiotics)
- Formal languages, finite automata and regular expressions
- Tries and related data structures (reifying functions on strings)
- Lambda calculus, types and type theory
- Some references on the Collatz ("3n+1") problem