[Agda] [lean-user] Why dependent type theory?

[Colin Stebbins Gordon]

You might be interested in Lamport and Paulson's "Should Your Specification
Language Be Typed?" (https://dl.acm.org/doi/10.1145/319301.319317).
Lamport's publications page includes some commentary on how the paper came
to be.


-Colin

On Tue, Mar 3, 2020, 14:44 Jason Gross <jasongross9 at gmail.com> wrote:

> I'm in the process of writing my thesis on proof assistant performance
> bottlenecks (with a focus on Coq), and there's a large class of performance
> bottlenecks that come from (mis)using the power of dependent types.  So in
> writing the introduction, I want to provide some justification for the
> design decision of using dependent types, rather than, say, set theory or
> classical logic (as in, e.g., Isabelle/HOL).  And the only reasons I can
> come up with are "it's fun" and "lots of people do it"
>
> So I'm asking these mailing lists: why do we base proof assistants on
> dependent type theory?  What are the trade-offs involved?
> I'm interested both in explanations and arguments given on list, as well
> as in references to papers that discuss these sorts of choices.
>
> Thanks,
> Jason
>
> --
> You received this message because you are subscribed to the Google Groups
> "lean-user" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to lean-user+unsubscribe at googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/lean-user/CAKObCaqa5NZvJvU_ZpZek%2BOnVEOQETiYpisbgJXhPchMn6PLcQ%40mail.gmail.com
> <https://groups.google.com/d/msgid/lean-user/CAKObCaqa5NZvJvU_ZpZek%2BOnVEOQETiYpisbgJXhPchMn6PLcQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200303/4424bdf2/attachment.html>