Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Why dependent type theory?
  • Date: Wed, 4 Mar 2020 10:07:55 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Pierre.Courtieu AT cnam.fr; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f47.google.com
  • Ironport-phdr: 9a23:Ug46rhwRdV1oTC/XCy+O+j09IxM/srCxBDY+r6Qd1OMRIJqq85mqBkHD//Il1AaPAdyHrasc1KGP6f2ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLx/IA+roQnNtMQajpZuJrgxxxDUvnZGZuNayH9nKl6Ugxvy/Nq78oR58yRXtfIh9spAXrv/cq8lU7FWDykoPn4s6sHzuhbNUQWA5n0HUmULiRVIGBTK7Av7XpjqrCT3sPd21TSAMs33SbA0Ximi77tuRRT1hioLKyI1/WfKgcFrkqlVvAyuqAB+w47MYYGaKvx+fr/GfdgHQWZNR9tdWzBdDo+5aYYEEugPMvtCr4TlqFQOoxmxCwmiCu3s1zFGmGP50LYg3Og9CwzLxhAsE84MvXnSsd77NL0SUeewzKTQ1zvDbu1Z2S3n6IfWbxssv/aMXa9qccrNyEkgCR7FhUiXpIL/PjOayP4Ns3KF4OZ6S++vjHMnqxttojiu2Mgsl5LEiZ4Tyl/e8CV12og1JcehRUN9fNWqE4NQujmEO4dqRs4uWWJltSYgxrEbuJO2fTIGxZslyhPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq9Eiv0Oz8Vs2t3FZLqSpJj8DAtn4C2hHR8MSHRfx9/kCu2TaLyQ/f8P1LIUcxlabDKp4hxKA/loYLvEjdAiP7nF/6gayWe0k+5+Sl6uXqbq/pq5KeL4N0jxvxMqUqmsyxG+Q4NQ0OUnCD+eS9yrLj51f5T6tQgvIqlanZrYraJdgapqGnHg9YyYkj6xOlADen1NQUh2UILFVAeB6flYjmJ0nOIOzkDfe4m1mjjDBrx+nfMrL9BpXNM2PMnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tNzCXVcFNFmfxP+vI9Fg3MtKUmWWR6SdLan6sFmS5+tpLfPaN6EPvzOoE/ko/eTjxVQ+hEUBfKS0lc8vaX2iBPkgCEKEe2btj8opGmEDu0wwVrq52xW5TTdPaiPqDOoH7TYhBdfjVN+bH9z/sPm6xC6+W6ZuSCVeEFndQ3zufoDCVe1eMHvPcP8kqSQNUP2ac6Fk1Ryqs1Wnmb9uL+6R+ypB8Jy/i5564OrckRx0/jtxXZzEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPEqjPlRFNgV7PRMAF43



Le mer. 4 mars 2020 à 09:00, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> a écrit :

> That is kind of a circular argument: Dependent types require your
> functions to be terminating, and termination requires dependent types to
> be proved, thus dependent types are required.

Well yes that is true. But the motivation for having termination
of all functions goes beyond having dependent types, eg consistency.

This sounds again like a circular argument: type theory generally needs termination for consistency, type theory helps for termination proofs, so type theory is good.
P.  

Archive powered by MHonArc 2.6.18.

Top of Page