Home

Welcome to the λC+ wiki!

You can play with our interpreter here!

For users

To learn how to use the language, you first need to know something about the Curry-Howard correspondence because λC+ is a proof assistant grounded in this correspondence. You can head on over to here to learn more about this. There, we provide a summary of the various quantifiers in λC+ and how they can be used.

Once you gain some familiarity with the subject, you can now begin learning to use λC+! This wiki page contains a detailed introduction to λC+.

For the theoretically inclined

If you're familiar with how to use the language and would like to take a peek at the underlying theory and semantics, you can head here.

For developers

This page gives an overview of our project and how to get started with hacking on it.