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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.