[Agda] [Coq-Club] Why dependent type theory?

[Jeremy Avigad]

I'd like to post a correction to my previous correction regarding the
origins of the use of implicit arguments in dependent type theory. In fact,
Section 7.2 of the 1985 paper on the Calculus of Inductive Constructions by
Thierry Coquand and Gérard Huet gives a very clear presentation of the idea
of using implicit arguments:

  https://www.sciencedirect.com/science/article/pii/0890540188900053

Thierry Coquand pointed out to me that Appendix 9 of the thesis of Jutting
(1977) describes a system AUT-SYNT that is a variation of Automath with
implicit arguments. This appendix is reproduced in the book on Selected
Papers on Automath:


https://www.google.com/books/edition/Selected_Papers_on_Automath/6pObdqwF0coC

It's nice to have the opportunity to call attention to these important
sources.

Best wishes,

Jeremy

On Mon, Mar 9, 2020 at 8:55 PM Jeremy Avigad <avigad at cmu.edu> wrote:

> Friends,
>
> In a footnote in a survey article I mentioned in this thread, I wrote that
> Amrokaine Saibi credited Peter Aczel with the idea of using
> implicit arguments in dependent type theory. James McKinna pointed out to
> me that I got this wrong: Saibi explicitly credits Randy Pollack for that.
> The Saibi article is here: https://dl.acm.org/doi/10.1145/263699.263742.
> The Pollack article is here:
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.7361.
>
> I feel bad for disseminating false history! I will correct the footnote in
> the arXiv version of the survey.
>
> Best wishes,
>
> Jeremy
>
>
>
> On Mon, Mar 9, 2020 at 2:30 AM Gabriel Scherer <gabriel.scherer at gmail.com>
> wrote:
>
>> In this nice quote, foundations are considered from the perspective of
>> expressive power:
>>   What if we find mathematics that *cannot* be formalized with our choice
>> of foundations?
>> In our experience with proof assistants, the discussion is generally not
>> about expressive power (the possibility to formalize something at all) but
>> about convenience, which in practice determines feasability:
>>   What if we find mathematics that cannot be formalized *in practice* by
>> our proof assistant, due to our choice of foundations?
>>
>> It is not obvious to me whether this impact of foundations on practical
>> usability of proof assistants is going to stay, or whether it is a problem
>> of youth that will go away as we develop better assistants. I would rather
>> hope the latter: that we can build proof assistants that are flexible
>> enough to conveniently support a very broad range of mathematics.
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200316/8acd2657/attachment.html>