[Agda] Using Agda in proving computer system correct
Marko Dimjašević
marko at dimjasevic.net
Mon Aug 5 10:56:54 CEST 2019
On Sat, 2019-08-03 at 21:22 +0200, Nils Anders Danielsson wrote:
> On 03/08/2019 10.05, Marko Dimjašević wrote:
> > Is it due to sub-optimal automated proof search?
>
> I don't know what the people you talked to had in mind, but this
> could
> be one thing.
What would you recommend for reading about Agda's support for automated
proof search? What is its current state?
> Libraries might be another.
Do you have any specific libraries in mind that would be useful for
proving properties of non-trivial computer systems? Do they exist and
if so, what kind of improvements they could use?
--
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
PGP key ID: 056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190805/80243e84/attachment.sig>
More information about the Agda
mailing list