coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Verification of CBV machine

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Verification of CBV machine
Date: Wed, 7 Mar 2018 18:58:35 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=smolka AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=smolka AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Ironport-phdr: 9a23:UcvtTxLby6OhmGE2s9mcpTZWNBhigK39O0sv0rFitYgRLv3xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicbODA2/27Zl89+gqxFrhymvBF/35fUYISJOPp+Yq/Qf9UXTndBUMZLUCxBB5uxYYoRAOobIeZTspTzp14JrRu6BgmjHv7kxzhThn/z2q061+chHhvd0Qw4BNICqmnUrNP0NKsLSuC61rPHzS/Hb/xM3zfy9ZLEfQ0/rvyVW797bMnfyVE3Gg/YgFidppbpMjeU2+gXsWWX9fRsWOK3h2I6pQx8rSKjy8Mth4XTm44YyVHJ+T9kzIopOdG1TlNwb8S+H5tKrS6aMpN7QsM8TGFsvyY30qEGuYS6fCgWz5QnwQTTa+aGcoSS/xLjUueRLS5jhH1/Yr2/nRKy/lKmyuLhTMW7zUhFojJEktnKqH8NywTe5tWJR/Zy5Eus3TeC2xrR5+1eP0w5lbLXK5s7zb4xkpoTv17DHijzmEjul6+Wc0Ik+uyr6+v9ebjmvoScO5VpigH4M6Qig9e/Dv4iPQgUW2iU4+K826D58ULkXrpGluc2nbXBsJDGOcQboba0DBNS0oY68hqwEzOm0MkDknQcN1JEeBeHj5DzNF3UIfD4C+2/g1W2nztxyfDGJO6pPpKYJX/a1bzlYLxV6khGyQN1w8oMyYhTD+QuLejvEnT0s9jbB1dtKAmzx+XuIM1mkJ4YWCeUC6aDNKrUvRmE67R8cKG3eIYJtWOleLAe7Pn0gCphwA5PTeySxZISLUuAMLFjKkSdb2Drh41ZQ38R+Bc4TanxgVSYVTdVazC+UvBlv21pOMedFY7GA7uVrvmZxi7hRs9OfSZbDFHJCn7hbYGNXftKZC/AepY8wAxBbqCoTsoa7T/rtAL+zOA4fPbO+zEfs9T5xp5o4eyWjhg77zh9Ccjb32zfF2w=

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