coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ANN: A Redex model of CIC

From: "William J. Bowman" <wjb AT williamjbowman.com>
To: coq-club AT inria.fr, Racket Users <racket-users AT googlegroups.com>
Subject: [Coq-Club] ANN: A Redex model of CIC
Date: Thu, 19 May 2016 13:37:43 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wjb AT williamjbowman.com; spf=Pass smtp.mailfrom=wjb AT williamjbowman.com; spf=None smtp.helo=postmaster AT mail.williamjbowman.com
Ironport-phdr: 9a23:VMjzdhefj+1abmjwlbNlOUVFlGMj4u6mDksu8pMizoh2WeGdxc+7YR7h7PlgxGXEQZ/co6odzbGG4ua7AydZucnJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuIOU4R3GX1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S4XVXxTmR5VCSDE6gv7V9H/qG+yjON22ySGdfDtQKovEWC45qxoRQOtlTwKLSUR/2bQhch9g7hcvQq64Rd4xtiHTpuSMa80QaLZedITQCJjGI57UDNEC4X2J98QDeApIudcq4j0olkEqgS7DA/qD+TqnGwbzkTq1LE3hrxyWTrN2xYtSpdX6CzZ

To understand CIC, I have been working through the CIC spec. in the Coq
reference manual and building a model in Redex.
The model is now fairly complete, and I thought it may be of interest to
these two lists, so I put the
model on GitHub:

https://github.com/wilbowma/cic-redex

Please free to study, improve, extend, or otherwise use it in anyway you see
fit. If you find mistakes
in the model, please let me know so I can correct my understanding.

--
William J. Bowman
Northeastern University
College of Computer and Information Science

Attachment: signature.asc
Description: PGP signature

[Coq-Club] ANN: A Redex model of CIC, William J. Bowman, 05/19/2016