Loading...
Please wait, while we are loading the content...
Similar Documents
Polytypic programming in COQ
| Content Provider | ACM Digital Library |
|---|---|
| Author | Hughes, Arthur Verbruggen, Wendy de Vries, Edsko |
| Abstract | The aim of our work is to provide an infrastructure for formal proofs over Generic Haskell-style polytypic programs. For this goal to succeed, we must have a definition of polytypic programming which is both fully formal and as close as possible to the definition in Generic Haskell. In this paper we show a formalization in the proof assistant Coq of type and term specialization. Our definition of term specialization can be interpreted as a formal proof that the result of term specialization has the type computed by type specialization. |
| Starting Page | 49 |
| Ending Page | 60 |
| Page Count | 12 |
| File Format | |
| ISBN | 9781605580609 |
| DOI | 10.1145/1411318.1411326 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2008-09-20 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Coq Theorem proving Polytypic programming Formalization Kind-indexed types Generic programming |
| Content Type | Text |
| Resource Type | Article |
