coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] algorithm complexity in Coq

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] algorithm complexity in Coq
Date: Tue, 19 Mar 2019 15:08:10 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f50.google.com
Ironport-phdr: 9a23:BRKqJh8LKxEOgf9uRHKM819IXTAuvvDOBiVQ1KB30OMcTK2v8tzYMVDF4r011RmVBN2ds6sMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5oHfbx9UiDagfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsVSmpPXMlfVyJPDIChYYURE+UPMv1Vr5Xkp1YUsReyGRWgCeHpxzRVhnH2x6o60+E5HAzbxgMgBM8FvmnMrNX0KKcSTf66zLPTzT7eaP5Zwi3x55LSfhEvu/2MRqpwccvNyUkzCQzFlE6QpJfqPzOQzOsNsmyb4/B8WuKojm4qsgd8qSWhyMcrj4nGnIMVylbc+Cpn3ok1Idy4SFVhbd6iDpRQqzmWN5BqTcMjXW5ovjo1xaMbtp66ZigF1ogoxwLFZ/ObdIiI5xTuX/uSLzdgnH9pZq6zihKo/UWjyuDwTNS43VdXoiZfktTAqnYA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5la/BJJ4gxr48j5oSsEreEiPvlkX7jLOael8r+uiv7OTnbbHmqYGGO4BojQH+N7wims25AesmLggDR3aX9fi42bH5/kD0QK9GguA3n6XEqpzXJdgXqra8AwBP04Yj7xi/Dy2h0NQdhXQIN0hJdwidg4nnIV3OO+j4Dfajg1Swjjhr3evGM6buApXINHfDkbPhcaxh5E5bzQo/1cpf6I5MCrEdPPLzXVf8u8DfDh8gKgC73+LnCMhm2Y4FQmKOAqqZMLvIvlOS5+IvJfOMZI4PtzrnJfgl/a2msXhsslgENYKtwJFfPHu/B7FtJ1iTSXvqmNYIV2kQ6FkQVuvv3XeLSnZof3euQ68m/XlvAsSvS5iFXZisnKCMxjyTEZhfZ2QAAVeJRyS7P76YUusBPXrBavRqlSYJAP34E9d4hEOe8TTiwr8iFdL6vygRtJbtzt9wvrSBmhQ79DgyBMOYgTjUEzNE21gQTjpz55hR5FRnww7ag6d9iv1cU9dU4qERC1poBdvn1+V/TuvKdEfBc9OOEgv0R9ynBXQgUYt0zYJWJUl6HNqmg1bI2C/4W7I=

A Coq library for internal verification of running-times
https://www.sciencedirect.com/science/article/pii/S0167642317300941

On Tue, Mar 19, 2019 at 2:52 PM Stefan Ciobaca
<stefan.ciobaca AT gmail.com>
wrote:
>
> Dear all,
>
> I'm looking for work related to formalized complexity analysis of
> algorithms in the Word RAM model.
>
> Something along the lines of http://www.eelis.net/research/quicksort/, but
> where the algorithm is formalized as a Word RAM machine, instead of using a
> shallow embedding. I would also be interested in other models of
> computation (e.g., Turing machines), preferably coming with a framework for
> reasoning in the model.
>
> I would appreciate pointers to any related item.
>
> Best,
> Stefan
>

[Coq-Club] algorithm complexity in Coq, Stefan Ciobaca, 03/19/2019
- Re: [Coq-Club] algorithm complexity in Coq, Bas Spitters, 03/19/2019