coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Verification of CBV machine

From: "Ramsdell, John D." <ramsdell AT mitre.org>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Verification of CBV machine
Date: Wed, 7 Mar 2018 18:47:30 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ramsdell AT mitre.org; spf=None smtp.mailfrom=ramsdell AT mitre.org; spf=None smtp.helo=postmaster AT smtpvmsrv1.mitre.org
Ironport-phdr: 9a23:JirsOxGZ2Xdfr9qQRqFH1J1GYnF86YWxBRYc798ds5kLTJ7zo8iwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBNxwo7bfI6bO/Vlc6PBZtwaQHZNUtpLWiFDBI63cosBD/AGPeZdt4TxqUcAogG7BQm3Gezg1DtIhnvu0aYn1+ohFgHG3Ao9FNwAqnjYosj+OaAIUe+vyanI1ijMYO1S2Tf584XIdxEhoe2WXb1ua8bRzlMvFwzcg1iWtIfrMTSV1uEXvGia6eptTeSvhHA6qw1rvDeg29osh4/UjYwW0lDJ7Th1zYIrKdGiSEN3f8SoHIZUuiyVLYd6X80vTmBwtConzrAKp4S3cDULxZg73RLSa+GLf5KL7x/nTOqRLyl3iXF5dL+6ghu97VWsx+LmWcSx0VtHritIn9rJu30C0xHe69aIR/5/80i6xDmAygbe4fxeL08uj6rUMZshz6YwlpUNtUTDGTf7mF7zjK+KbkUk5O2o6//9YrX4u5OQLYp0igDiMqQ0hMOzG+M4MhIBX2SD+OS80qPs/VHhTblXivA6jLPVvZDEKcgBu6K0BwBY3pw+5xuxDjqqyNEYkmMGLFJBdhKHlY/pO1TWLfDiF/i/hk+snyp1yPDCOr3sGZDNLnnfkLf7Y7lx8UlcyBA8zdxH/ZJbFqkBIO7vWk/2rNHXEhg5MxWtz+n7DNV9y5gRVHmUAq6ZNaPSqUWH6vguI+mKfo8VuSzyJ+Ir5/703jcFngpXdq6wmJATdXqQH/J8Ikzfb2CmyoMKFn5PtQ4jRsTrjkeDWHhdfSDhcbg742RxMoujFovOQoTpyJ6G3CHzMtscLjRcA1WXHXrsc62BWusWZWSVOMA3wW9MbqSoV4J0jULmjwT90bcydrOFqB1djorq0Z1O38OWkBgz8TJuCMHEijOITn1ukyUPXTBkhPkj83w48U+K1O1Du9IdDcZavqobVwYmL5OayPZ1WYirB1DxO+yRQVPjee2IRDE8StVrmY0VZlplBdC5lA6amS+rH6UY0buRC85s/w==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

I did a proof of the SECD machine in NQTHM. The work was published in the
Journal of Automated Reasoning in 1999.

http://www.ccs.neu.edu/home/ramsdell/papers/trsecd.pdf

John

-----Original Message-----
From:
<coq-club-request AT inria.fr>
on behalf of Gert Smolka
<smolka AT ps.uni-saarland.de>
Reply-To:
"coq-club AT inria.fr"

<coq-club AT inria.fr>
Date: Wednesday, March 7, 2018 at 12:59 PM
To:
"coq-club AT inria.fr"

<coq-club AT inria.fr>
Subject: [Coq-Club] Verification of CBV machine

We are verifying a machine for CBV lambda calculus in Coq.
The machine is stack-based and represents terms as closure on a heap.
Our goal is to come up with an elegant formalisation and verification
both on paper and in Coq. We follow a refinement approach and
consider programs, closures, and heap in successive refinement steps.

I would appreciate pointers to related work. Our main interest
is in the formulation and presentation of the correctness
statements and proofs. We are familiar with Plotkin’s
1975 paper, of course.

Gert

[Coq-Club] Verification of CBV machine, Gert Smolka, 03/07/2018
- Re: [Coq-Club] Verification of CBV machine, Reynolds, Thomas N. (MU-Student), 03/07/2018
- Re: [Coq-Club] Verification of CBV machine, Ramsdell, John D., 03/07/2018