The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

More broadly, categorical semantics benefits from things like W-types, which 
are difficult to construct without an appeal to Adamek’s construction, which 
requires (in set theory as well as dependent type theory) quotients.

Sent from my iPhone

> On Jan 3, 2020, at 8:55 AM, Thorsten Altenkirch 
> <Thorsten.Altenkirch AT nottingham.ac.uk>
>  wrote:
> 
> Quotient reasoning isn’t used enough in program verification because we 
> are used to think in terms of syntax missing many tricks which are based on 
> a more semantic perspective and which lead to nicer structures. An example 
> is the treatment of non-termination which is often addressed by some fuel 
> based approach. We have shown that non-termination is a monad given by the 
> free omega-cpo over a given set (in the sense of HoTT) using a quotient 
> inductive type. More needs to be done but there is the potential to 
> actually use the ideas from domain theory in practical program verification.
> 
> Sent from my iPhone
> 
>>> On 3 Jan 2020, at 13:34, Adam Chlipala 
>>> <adamc AT csail.mit.edu>
>>>  wrote:
>>> 
>>> On 1/3/20 7:37 AM, Thorsten Altenkirch wrote:
>>> Both Coq and Lean fail in properly supporting structures with a 
>>> non-trivial equality. Lean doesn’t really offer an answer to setoid hell 
>>> but just adds quotients as an axiomatic principle with no computational 
>>> explanation. This is despite us knowing since a while (I wrote a paper on 
>>> this in ’99) how to turn setoid hell into setoid heaven by working within 
>>> the setoid model: that is if you want to talk about setoids all the time 
>>> just accept that every type comes with its own eqaulity and build your 
>>> type theory around this.
>> I think one factor that might lead to surprisingly different perspectives 
>> from different people in this discussion is that, as far as I can tell, 
>> quotient reasoning is much more common in pure math than in program 
>> verification.  Yes, it comes up often enough that everyone working on 
>> program verification has used it in a few projects, but it hardly seems to 
>> rise to the level of an essential foundation for all work (which raises 
>> questions of whether it is worth complicating the core type theory to 
>> support, expanding the trusted base).  I don't think too many 
>> program-verification projects are avoiding quotient reasoning because it 
>> is awkward rather than just not especially applicable.
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
>