Mercurial > cpdt > repo
changeset 464:e53d051681b0
Finish complete proofreading pass
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 29 Aug 2012 17:17:17 -0400 |
parents | 218361342cd2 |
children | 4320c1a967c2 |
files | latex/cpdt.bib src/ProgLang.v |
diffstat | 2 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/latex/cpdt.bib Wed Aug 29 17:03:19 2012 -0400 +++ b/latex/cpdt.bib Wed Aug 29 17:17:17 2012 -0400 @@ -17,7 +17,7 @@ title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm}, journal = {IEEE Transactions on Computers}, volume = {47(9)}, - pages = {913--926} + pages = {913--926}, year = {1998} } @@ -162,7 +162,7 @@ title = {Higher-order abstract syntax}, booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation}, year = {1988}, - pages = {199--208}, +% pages = {199--208}, } @article{HOU, @@ -300,7 +300,7 @@ title = {How to make ad-hoc polymorphism less ad hoc}, booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, year = {1989}, - pages = {60--76}, +% pages = {60--76}, } @inproceedings{reflection,
--- a/src/ProgLang.v Wed Aug 29 17:03:19 2012 -0400 +++ b/src/ProgLang.v Wed Aug 29 17:17:17 2012 -0400 @@ -330,7 +330,7 @@ | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2. ]] - However, Coq rejects this definition for failing to meet the %\index{strict positivity restriction}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic. + However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic. An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq. Here the idea is to parametrize the syntax type by a type family standing for a _representation of variables_. *)