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 MCMP 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:

Interactive Exercises

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.

Visual Derivations

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.

Grade Management

Students may submit completed work electronically, which is automatically scored by the calculator.

Immediate Feedback

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.

Thanks to an NYU CDCF grant awarded in the spring of 2013, 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 Lambda Abstractions over arbitrarily-typed indices
  • 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.

Arnim von Stechow, Professor Emeritus, Department of General Linguistics, Tübingen, Germany

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.

Jae-Woong Choe, Professor, Department of Linguistics, Korea University, Seoul

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.

Gerhard Schaden, Maître de Conférences, Université Lille 3 Charles de Gaulle, Paris

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.

Hilton Alers, Associate Professor, University of Puerto Rico

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 work.

Penka Stateva, Assistant Professor, University of Nova Gorica

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 feature.

Ezra Keshet, Assistant Professor, University of Michigan

Downloading and Installing

You can download the current student version 2.1.0 (December 7, 2015; Change Log) by clicking the icon for your operating system below.

Latest Stable Release:
Download older version for Windows and Mac/Linux

For Mac and Windows: just download and double-click to start. If you are running OS X 10.7.5 (Mountain Lion) or later, you may need to temporarily relax your security settings to open the application, since it is not from the Mac App Store. In System Preferences > Security & Privacy > General, set "Allow applications downloaded from:" to "Anywhere". After opening and quitting the app once, you may adjust the setting as you like. For Linux: start with java -jar LambdaCalculator.jar, but make sure you run it with Sun's Java, not GNU libgcj. You can check which version you have with java -version.

Installing Java

Windows and Linux users will need to make sure they have the Java JRE 1.6 or newer installed. The Windows version of the calculator will check on startup if Java is installed, and if necessary, will take the user to a website where Java can be downloaded.

Teacher Edition

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 email to:

Sample Exercises

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 instructors.

Basic Examples

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. 5 -- Relative Clauses, Variables, Variable Binding

Ch. 6 -- Quantifiers: Their Semantic Type

Ch. 7 -- Quantification and Grammar

Ch. 8 -- Syntactic and Semantic Constraints on Quantifier Movement

You can find many more examples at the calculator's Wiki

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 Github 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.

More Information

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.