coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kenneth Adam Miller <kennethadammiller AT gmail.com>
- To: coq-club Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Atomic types?
- Date: Tue, 1 Dec 2015 11:13:59 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kennethadammiller AT gmail.com; spf=Pass smtp.mailfrom=kennethadammiller AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f170.google.com
- Ironport-phdr: 9a23:tQDDShxIy042DTzXCy+O+j09IxM/srCxBDY+r6Qd0eIeIJqq85mqBkHD//Il1AaPBtWFraocwLeI+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU15z8ir760qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jgsgCGRg+S7DM3Vngc2k5DBBGA5xXnVL/wtDH7v6xzwn/JE9fxSOUXVDKk4rtrADbkgSJPEj899GzNwphzgaRdrQ6hrhB2xovVZIWYLtJxe6rceZURQm8XDZUZbDBIHo7pN9hHNOEGJ+sN6tCl/1Y=
I have a very simple use case for Coq and I work in software security. We'd like to have a core component of our software model reside in the untrusted computing base, and so it's attractive to be able to do this with Coq.
However, concurrency is very much a part of what our system must address. With some atomic types, however, this can be totally addressed. I'm not aware of any atomic types or even a type level notion of concurrency such as a process calculus or otherwise in Coq. Is anybody else?
However, concurrency is very much a part of what our system must address. With some atomic types, however, this can be totally addressed. I'm not aware of any atomic types or even a type level notion of concurrency such as a process calculus or otherwise in Coq. Is anybody else?
- [Coq-Club] Atomic types?, Kenneth Adam Miller, 12/01/2015
Archive powered by MHonArc 2.6.18.