The Lambda Calculator is an interactive, graphical application
to help students of natural language semantics practice derivations
in the typed lambda calculus. It is designed for both students and
teachers, with modules for online classroom instruction, graded
homework assignments, and self-guided practice. The primary function
is to assist in the computation of natural language denotations up a
syntactic tree in the style of Heim & Kratzer (1998). To this
end, the program detects common errors and attempts to provide
intelligent feedback to the student user and a record of performance
for the instructor.
This split-screen video of a talk on
the interaction of
compositional semantics and event semantics gives an impression
of many of the features of the calculator and how it can be
dynamically integrated into presentations. The calculator is used
starting at 17:39 to step through various derivations. (Thanks to
Kristina Liefke and Roland Poellinger of the
for providing the video.)
The core of the program is described in our contribution to the
proceedings of GEAF 2007:
Champollion, L., J. Tauberer and M. Romero (2007). "The Penn
Lambda Calculator: Pedagogical Software for Natural Language
Semantics", in T. Holloway King and E. M. Bender (eds.),
Proceedings of the Grammar Engineering across Frameworks (GEAF)
2007 Workshop, July 13-15 2007. CSLI On-line Publications [PDF]
A sample of the features discussed there:
Students progress through pre-prepared exercise files, checking
types and reducing lambda terms. As they go, their answers are
evaluated for correctness, and the program gives feedback.
Instructors can present bottom-up derivations step-by-step. At
any point, derivations may be interrupted or rewound, or re-run
with modified lexical entries.
Students may submit completed work electronically, which is
automatically scored by the calculator.
Students receive feedback after each step of a derivation or
reduction. When they make mistakes, the program attempts to guess
what went wrong and provide suggestions.
Export to LaTeX
The program provides an option to export any tree as LaTeX
source code, in a format accepted by Qtree and tikz-qtree.
The program now includes flexibility for types in a variety of uses:
More flexible composition rules, including
Predicate Modification and
Intensional Function Application
Traces and Predicate Abstractions over
Type variables for
polymorphic lexical items and combinators
[The Calculator] covers most of the common ground of formal
semantics and it is great fun using it, and the notation is
compatible with many introductions to semantics, e.g. the book of
Heim and Kratzer. Students working with that tool will love it and
possibly fall in love with formal semantics of natural language. I
always wanted to have such a tool for my teaching.
I learned about the program toward the middle of the semester, but
once I knew about and briefly tested it, I did not hesitate to
introduce it to the class. [...] Had I known about the program
before I prepared my syllabus for the class, I definitely would
have designed my class so that we can make use of the program more
extensively. I would recommend PLC to anyone who is willing to
explore some better ways to teach and learn the sometimes tedious
and confusing work of lambda derivations.
I wished it had already existed at the moment when I made my first
steps in formal semantics; certainly, I would have learned faster
and easier. One can only master the lambda calculus (and formal
linguistics in general) by getting one's hands dirty, that is, by
experimenting and testing. The calculator provides students with
hints and immediate feedback whether their proposed solution is
correct or not.
I am very grateful for your having the Penn Lambda Calculator so
generously available to teachers and students of Formal Semantics.
As an instructor of a graduate-level course using Heim &
Kratzer (1998), I can attest how invaluable this resource has been
for both me and my students as well. The lambda notation is not
easy for students who, despite their linguistics training, are not
familiar with the formal apparatus of set theory, propositional
calculus and predicate logic. As I teach to Spanish-speaking
students, it adds to the inherent difficulty of the subject the
fact that the textbooks and the exercises included are mostly in
English. With the lambda calculator I can create exercises using
lexicon (and instructions) in Spanish that allow my students to
practice how to simplify lambda expressions and calculate the
denotations of syntactic trees at home. In the classroom it makes
it possible to discuss problems that will take forever otherwise.
I found the Calculator especially helpful for the individual
training of students during recitations. It allowed each of them to
follow their own pace. Students were all very positive about using
it mostly because it is an interactive tool and provides intelligent
feedback. The course is based on the Heim and Kratzer 1998 textbook
Semantics in Generative Grammar which makes the tool a very
valuable asset not only because it is designed to accompany that
textbook but also because the textbook itself puts an accent on
practice and exercise for mastering the calculating techniques and
internalizing the principles behind them. In short, this is an
excellent pedagogical tool which I will continue using in my future
The software is groundbreaking and ingenious — no one has
written anything like it before and it is well-designed to fit into
a formal semantics course. I especially like the guidance it gives
students when they make mistakes — that was a very clever
Downloading and Installing
You can download the current student version 2.6.0 for Mac/Linux/Windows (August 31, 2022; Change Log) by clicking the icon
for your operating system below.
For Mac: download the .dmg file, locate the downloaded .dmg in Finder and right-click or Ctrl-click to open,
and select "Open Anyway" if Mac complains that the developer isn't verified.
Then, drag the application to the "Applications" folder or wherever else you like.
The first time you launch the application, right-click or Ctrl-click on it
and select "Open" from the shortcut menu.
After opening and quitting it once in this way, you
can launch it simply by double-clicking.
For Windows: download the file and unzip. Enter the resulting folder called LCSE. It contains
an .exe file and a subfolder called jre180 which contains a Java runtime environment.
Double-click on the .exe file to start. As long as the
.exe file and jre180 are kept in the same folder, the application
will run out of the box with no need to install Java separately. Unless you have a separate Java runtime environment
installed on your computer, do not move the exe file out of the LCSE folder, and do not move
or delete the jre180 folder.
For Linux: make sure you have either Oracle's java or
openjdk installed, in each case version 1.8
or higher. (Avoid GNU libgcj as this will not work.) You can check which version of java you have with
java -version. To launch the application, type java
The teacher edition, in which tree-derivation exercises can be shown
in a presentation mode that automatically computes denotations of
nonterminals, is available upon request to instructors. Please send an
These documents provide some basic exercises to get you started.
Just download any of the files above (or copy and save the text to a
blank text file of your choosing). Then run the Lambda Calculator,
select Open from the Menu Bar, and open the exercise file you saved.
If you are an instructor, email us, and we will be happy to send you
more exercise files. And if you write exercise files yourself,
please consider sending them to us so we can share them with other
Examples of 'semantic types' and 'lambda conversion' exercises
Examples of bottom-up tree derivation exercises
Examples of using bottom-up tree derivations with generalized
quantifiers (including set notation).
Examples from Heim & Kratzer
Ch. 3 -- Semantics and Syntax
Ch. 4 -- More of English: Nonverbal Predicates, Modifiers, Definite Descriptions
Ch. 8 -- Syntactic and Semantic Constraints on Quantifier Movement
You can find many more examples at the calculator's
Issues and Suggestions
The calculator is under active development, and may exhibit
unexpected behavior from time to time, especially if you're using
one of the Beta releases. If you encounter something strange, or
would like to see some additional functionality, we're all ears. Our
bug reports and feature requests are managed through on our
Issues page. Please take a look at the open issues to see if
your problem has already been reported (and if so, to check the
progress on fixing it). You can report new issues or make new
requests directly through the Issues page, if you have a registered
Github account. Otherwise, just shoot us an email (),
and we'll create a ticket that you can monitor for updates. In
either case, include any information you can that will help us
reproduce the problem, including exercise files, screenshots, and
information about your operating system and the version of the
calculator that you're using.
Detailed instructions, sample exercises, frequently asked questions,
and bug reports are all available at this project's Github
Wiki. We are very interested in hearing about your
experience with the Lambda Calculator, and about potential ideas for
improvement, so please either head over to the wiki if you have
questions or suggestions, or send us an email.
Similar projects to the Lambda Calculator include: