Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts


Chronological Thread 
  • From: Denis Nikiforov <denis.nikif AT gmail.com>
  • To: Talia Ringer <tringer AT cs.washington.edu>
  • Cc: Coq-Club <coq-club AT inria.fr>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
  • Subject: Re: [Coq-Club] [isabelle] Abandoned proof engineering efforts
  • Date: Tue, 18 Feb 2020 17:58:18 +0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=denis.nikif AT gmail.com; spf=Pass smtp.mailfrom=denis.nikif AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f48.google.com
  • Ironport-phdr: 9a23:C9Fp0BWCpwxoMNqFAKC3ConRcL3V8LGtZVwlr6E/grcLSJyIuqrYbBGGt8tkgFKBZ4jH8fUM07OQ7/m8HzNQqsrf+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMg4ZvKak9xxTIr3BVZ+lY2GRkKE6ckBr7+sq+5oNo/T5Ku/Im+c5AUKH6cLo9QLdFEjkoMH076dPyuxXbQgSB+nUTUmMNkhpVGAfF9w31Xo3wsiThqOVw3jSRMNDsQrA1XTSi6LprSAPthSwaOTM17H3bh8pth69AvhmvuwJwzJLVYIGNNfpxYKXdfc8BRWFcWspdTjFNDp+gY4cKCecKIORWoJTnp1YWohS+CwujCuPhxDFLm3H4w7E13v87Hg3axgEtBc4CvGjWodjzKawcUfq1zK7NzTjbYf1ZxzH96InTchs8uf+MXLFwccvfyUkoDQPFiUuQopHiMjyIyOsNtWmb7/F6WeKpim4nqABxoja0y8cjj4nGnIMVylTe+Splx4Y1IMS1RUhmatCqF5tQsjuVN4pwQs46QmFoozw1xqQctp61ZCgG0pMnxwTQa/CffIiI4w7jVOaMIThjnn5qZLW/hxO0/EO9yeP8TtG53EhWoidBiNXBtXAA2wbN5sSZVPdx5Eis1DWJ2gvO8O9LO1o0mrDeK5M5wr4/iJ4TsUPbEy/zgkr2jauWelw5+uey9ujre7vmq5CfOoNuhQH+NaMumsO7AesmKAQBQ2+b+eGk2L3i+032XqlKg+UonqXFtJ3WP8cWq66jDwNLzIov9QyzAjil3dgAmHkINlNFeBaJj4jzPFHOJej1AuqhjFSqkTdr3OrKPrvgApXOL3jDnqzsfbl460FGyQozycpT6I5TCrEEOP7zQFP+tMTEDh8lNAy52/roCNJk1o8HRW2PBrKZP7jJvF+T5uMvJvGMa5UPtDb8Lfgl/f/ugmUjlV8TZ6n6lacQPUyxGvVva3+YZ3XhmJ9VDX0LuAUzVsThkxudWCVTZnC9Q6U6oDw3FdT1I53EQ9WBjbqAx2+dH55XaGdcDU7ERXvlcYSfHfENayOcCsBkmz0AE7OmTtlyhlmVqAbmxu8/faLv8SoCuMemjYAtvrGBpVQJ7TVxSv+l/SSVVWgtxzEHQjY32OZ0pkkvkg7eg5g9uORREJlo390MUgo+MsSBnelzCtS3RwuYO9nVGBCpRdKpBTx3RdU0kYdXMhRNXu66hxWG5BKERroclriFHpsxq/uO0H34JsI7wHHDhvAs

Hi

I formalized the semantics of the OCL language: https://www.isa-afp.org/entries/Safe_OCL.html
Here is a significantly improved version of the theory: https://github.com/AresEkb/Safe_OCL  
I added new data types, added a concrete syntax, refactored the type system and changed semantics of some operations after discussion with a main OCL contributor.

The project has two goals:
1) Provide a simple reference formalization of a real (non-toy) language for people far from mathematics (for engineers like me). There are a lot of examples of toy languages, but when you start to formalize a more complicated language it's not an easy task. Formalizations of other languages (Java, etc.) are too complicated for me.
2) Improve OCL language itself.

However, I don't have time to finish it. I hope I'll do it in future.



вс, 16 февр. 2020 г. в 06:28, Talia Ringer <tringer AT cs.washington.edu>:
Hi all,

I'm curious if any of you have ever started to verify a system, but then
abandoned that system due to the difficulty of evolving and maintaining
your proofs. If so, I would love for you to share those proof efforts with
me, especially if the code is public.

Thanks!

Talia



Archive powered by MHonArc 2.6.18.

Top of Page