[Agda] Small Kernel

[Yotam Dvir]

Hi there,

I am interested in the soundness of Agda as a proof-assistant. To my understanding Agda development veers more in the direction of interesting abstractions and advanced programming features, at the cost of less solid foundations.

Is this understanding correct?
How close is Agda to having a so-called "small kernel”, and how does it compare to other proof-assistants such as Coq and HOL Light?

(You are also welcome to answer on cstheory.stackexchange <https://cstheory.stackexchange.com/q/45665/54969>.)

Thanks in advance!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191203/d2716cdb/attachment.html>