[Agda] Termination checker and rewriting

[Guillaume Allais]

Let's not forget about confluence :)

On 29/01/2019 15:47, Thorsten Altenkirch wrote:
> I guess this shouldn’t be just a checker but a way to prove externally that the system is terminating using agda.
> 
> T.
> 
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Jesper Cockx <Jesper at sikanda.be>
> Date: Tuesday, 29 January 2019 at 14:42
> To: Nils Anders Danielsson <nad at cse.gu.se>
> Cc: agda list <Agda at lists.chalmers.se>
> Subject: Re: [Agda] Termination checker and rewriting
> 
> On 29/01/2019 13.57, Guillaume GENESTIER wrote:
>> More specifically, I was wondering if any termination checking is
>> performed on these rules.
> 
> No.
> 
> ... but if you are interested in working on implementing a termination checker for rewrite rules, send me a mail and let's talk.
> 
> -- Jesper
> 
> On Tue, Jan 29, 2019 at 2:19 PM Nils Anders Danielsson <nad at cse.gu.se<mailto:nad at cse.gu.se>> wrote:
> On 29/01/2019 13.57, Guillaume GENESTIER wrote:
>> More specifically, I was wondering if any termination checking is
>> performed on these rules.
> 
> No.
> 
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> 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.
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190129/69a24c9c/attachment.sig>