coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why dependent type theory?

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Why dependent type theory?
Date: Tue, 3 Mar 2020 14:09:42 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f178.google.com
Ironport-phdr: 9a23:squ2DRF1DwL6uras3FEC651GYnF86YWxBRYc798ds5kLTJ78oMWwAkXT6L1XgUPTWs2DsrQY0raQ6vi+EjVdsN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrogjdrNQajZdjJ6o+1xfEon9FcPlKyG11Il6egxnz6sCs8ZB57i9eoegh98lOUaX7e6Q3U7lVByk4Pm42+cPmqwDNQROA6XUAXGoWlAFIAxXe4xHhQpjxqCr6ufFj1yScIMb7UKo7WTWm76dsVR/olCIKPCM3/W3LlsB9ir9QrQm/rBJj3YHbfICVNOJ/fqzDe9MaWXFBVdtVWyBYH4+wc5cDA+8HMO1FrYfyukEOoAOxCgmiBuzhyjFGiHzr06Mkz+ssCh3G0BA6Et4SrHjYsNf4OaEPWu611qnIyjDDYutY1zjn7ojIcw4uofWRVrxtbcXRyVcgFxvBjlqOs4zuIjSY2fkWs2eH7+pvS/qvi2o5pAFruTWvycIshZPIhoIR0FzL6SJ5wIMsKNC+VUV1YsakHYNOuy2GM4Z6WMAvTmFytCony7ALuIS3cDUIxZkkwRPUduaJfJKS4h35UeacOTd4i2xheLK4nxuy9FKvyuz4VsWt0VZKqjdJnsDCtnwQ1RHe6dKLSvR6/kem1jaP0x7c5vtYLkAzkKrXM58hwrgumZoPqUnPADP6lUHsgKKVdkgo4PWk5uXmb7n8u5ORNYx5hhn7Mqs0m8y/Beo4MhIJX2ie4emzyabj8lH5QLpUlv02lrfWsIrBKMQUo662GQ5V0oI55xmjCDem1cwUnWMbI1JdZBKHk4/pNknSL/D/FPezmkijkDN2x//dJbDhGZXMLn3bkLj7Z7p96khcyBAyzd9F/Z5UBKsBc7rPXRras8WQJRskOUTgyOH+Td55y4k2WGSVA6bfPrmE4nGS4ed6D+CKZYIR8A32K/U94/P0xSs1glQdcLGt0IE/Z3WxH/AgKEKcNym/yuwdGHsH61JtBNfhj0ePBHsKPy7rDvAMowojAYfjNr/tA4WkgbiPxiC+R8QEaWVPC1TKGnDtJdzdB6U8LRmKK8okqQQqEKC7QtZ4hx6rvQ7+jbFgK7iMo3BKhdfYzNFwotbru1Qy+DhzVZrP1miMSyR1mjpNSWZpjOZwpktyzlrF2q990aRV

On Tue, Mar 3, 2020 at 11:44 AM Jason Gross
<jasongross9 AT gmail.com>
wrote:
> So I'm asking these mailing lists: why do we base proof assistants on
> dependent type theory?

The simple answer that came to my mind first, but which I haven't seen
so far, is: with the underlying theory CoC (or CoC plus?) being based
on the Curry-Howard correspondence, we require dependent types to be
able to express first-order logic statements such as forall x : A, P
x.
--
Daniel Schepler

Re: [Coq-Club] [Agda] Why dependent type theory?, (continued)
- Re: [Coq-Club] Why dependent type theory?, Christian Doczkal, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Ken Kubota, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, jonikelee AT gmail.com, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Daniel Schepler, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, mechvel, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Steven Shaw, 03/03/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Steven Shaw, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Martin Escardo, 03/03/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Sylvain Boulmé, 03/04/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Kevin Buzzard, 03/05/2020
    - Re: [Coq-Club] [lean-user] Re: [Agda] Why dependent type theory?, Bas Spitters, 03/08/2020
      - Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Thorsten Altenkirch, 03/12/2020
        
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Mario Carneiro, 03/13/2020
        
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Kevin Buzzard, 03/13/2020