Commit de133a57 authored by Adam Chlipala's avatar Adam Chlipala

Finish complete proofreading pass

parent 419e2d0e
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm}, title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
journal = {IEEE Transactions on Computers}, journal = {IEEE Transactions on Computers},
volume = {47(9)}, volume = {47(9)},
pages = {913--926} pages = {913--926},
year = {1998} year = {1998}
} }
...@@ -162,7 +162,7 @@ ...@@ -162,7 +162,7 @@
title = {Higher-order abstract syntax}, title = {Higher-order abstract syntax},
booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation}, booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
year = {1988}, year = {1988},
pages = {199--208}, % pages = {199--208},
} }
@article{HOU, @article{HOU,
...@@ -300,7 +300,7 @@ ...@@ -300,7 +300,7 @@
title = {How to make ad-hoc polymorphism less ad hoc}, title = {How to make ad-hoc polymorphism less ad hoc},
booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = {1989}, year = {1989},
pages = {60--76}, % pages = {60--76},
} }
@inproceedings{reflection, @inproceedings{reflection,
......
...@@ -330,7 +330,7 @@ Module HigherOrder. ...@@ -330,7 +330,7 @@ Module HigherOrder.
| Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2. | 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_. *) 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_. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment