[Agda] Termination checker and rewriting

[Thorsten Altenkirch]

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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190129/f4c7faed/attachment.html>