coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Verification of CBV machine

From: "Reynolds, Thomas N. (MU-Student)" <tnrn9b AT mail.missouri.edu>
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:37:26 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tnrn9b AT mail.missouri.edu; spf=Pass smtp.mailfrom=tnrn9b AT mail.missouri.edu; spf=Pass smtp.helo=postmaster AT NAM03-BY2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:gsOYchReCrY8ibrIGp1unw45udpsv+yvbD5Q0YIujvd0So/mwa6zZh2N2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO+FzcbnBcdMfX2dNQtpdWi5HD4ihb4UPFe0BPeNAooXzu1UBsxu/BQ+rBOPr1zBInWf61rAk3eQhFgHG2RYvH8kTu3rMttn+KaMeX+e7w6XR0DvDc+5W1irj54jObhAtpP+AVq93fMrNz0kvDQXFg1GLpoH+OjOazOUNs2yB4+plVOKvkHUnqwZsoji1x8cgkJfGiZ8Iyl3d8yhy3YU7JcWgRUJmfdKpH4Fcui6YOodsTc4uXXtktSY6x7EepJK3YisHxI45yxLDavGLaZaE7xL+WOqLPDt0mm5pdKqxhxms8kWs1ujxW8y03VtJrydIkNzBum4O2hzd9MSKT/tw80mi1DaB0g3e6/9ILEMvmqfdNpUv2KQ/loAJvkTGBiL2mFv5jKuRdkg84ual9+Ppbqnoq5OFKoJ7iB/yPr0pmsOkH+s0KA8OX3WH+eun073j4Ev5T6hQgv0uiKnZt4zaKtoHqa6lAg9V1YAj5wy4Dze7zNQYmX4HLFVGeB6dk4fpPFTOLOj5Dfe5nVusjC9my+3aMrDuGJnAIXrOnK3ucLpj8UJRyAo+wcha551OC7EBJPzzWlX2tNzdFhI5Lwq0w/zhCNh5zYwTQmePDbWYMKPWq1OI4+MvI/KXZI8SpTb9Mfkl6+TwgnAkhF8RZbOp0ocPaHCkAvRmJF2UbmbrgtcYCGsFog4+TPHxh1CZSj5SZ3OyX7om6T0hCYKmC53DRoG3j7Cb0ie7BM4eWmcTQFuLCDLjc5iOc/YKciObZMF72HRQXr+4DoQlyBuGtQngyrMhIPCCqQMCspe2nuJ49uvUkR0psXRID8OY2nrFaSc83kY1AgQqwaxyp1A8gB/Xza5iha1SPdla5vcPVwYhLpnB1e08BtzvDFGSNuyVQUqrF431SQo6Scg8lodXMhRNXu66hxWG5BKERroclriFHpsxq/OO2nHwI4B4ym3d07Q7jh8rTtYdbDT61J46zBDaAsvyq2vcj7yjLPVO2SfM8CGGzHGVu1xCUUh9XbiXBSlCNHuTlszw4wb5d5HrCbkjNVcem+irD/MRL/fY1xBBTvqlP8nCaWWsnWv2HQyP2r6HcIvtfSMawTnZD08H1QsU+CTfOA==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Robert Krebbers has some nice (but not completely related) work in this area. I think.

"coq-club-request AT inria.fr on behalf of Gert Smolka" <coq-club-request AT inria.fr on behalf of smolka AT ps.uni-saarland.de> 3/7/18, 11:59 AM:

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