1
$\begingroup$

I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf

The calculus, works and I experimented with it and like it. However, I want to add inductive types to do more complex stuff. What are the options for doing this?

I am thinking about two ways of doing so

  • Introduce Fin-N, Product and W-types and represent inductive types with them.
  • Generate induction and recursion axioms.

What can you recommend? How inductive types are represented in systems like Coq, Idris and Agda? Which articles can you recommend me?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.