1528 section {* Adequacy *} |
1528 section {* Adequacy *} |
1529 |
1529 |
1530 section {* Related Work *} |
1530 section {* Related Work *} |
1531 |
1531 |
1532 text {* |
1532 text {* |
1533 Ott is better with list dot specifications; subgrammars |
1533 The earliest usage we know of general binders in a theorem prover setting is |
1534 |
1534 in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of |
1535 untyped; |
1535 the algorithm W. This formalisation implements binding in type schemes using a |
|
1536 a de-Bruijn indices representation. Also recently an extension for general binders |
|
1537 has been proposed for the locally nameless approach to binding \cite{chargueraud09}. . |
|
1538 But we have not yet seen it to be employed in a non-trivial formal verification. |
|
1539 In both approaches, it seems difficult to achieve our fine-grained control over the |
|
1540 ``semantics'' of bindings (whether the order should matter, or vacous binders |
|
1541 should be taken into account). To do so, it is necessary to introduce predicates |
|
1542 that filter out some unwanted terms. This very likely results in intricate |
|
1543 formal reasoning. |
|
1544 |
|
1545 Higher-Order Abstract Syntax (HOAS) approaches to representing binders are |
|
1546 nicely supported in the Twelf theorem prover and work is in progress to use |
|
1547 HOAS in a mechanisation of the metatheory of SML |
|
1548 \cite{LeeCraryHarper07}. HOAS supports elegantly reasoning about |
|
1549 term-calculi with single binders. We are not aware how more complicated |
|
1550 binders from SML are represented in HOAS, but we know that HOAS cannot |
|
1551 easily deal with binding constructs where the number of bound variables is |
|
1552 not fixed. An example is the second part of the POPLmark challenge where |
|
1553 @{text "Let"}s involving patterns need to be formalised. In such situations |
|
1554 HOAS needs to use essentially has to represent multiple binders with |
|
1555 iterated single binders. |
|
1556 |
|
1557 An attempt of representing general binders in the old version of Isabelle |
|
1558 based also on iterating single binders is described in \cite{BengtsonParow09}. |
|
1559 The reasoning there turned out to be quite complex. |
|
1560 |
|
1561 Ott is better with list dot specifications; subgrammars, is untyped; |
1536 |
1562 |
1537 *} |
1563 *} |
1538 |
1564 |
1539 |
1565 |
1540 section {* Conclusion *} |
1566 section {* Conclusion *} |
1541 |
1567 |
1542 text {* |
1568 text {* |
1543 Complication when the single scopedness restriction is lifted (two |
1569 Complication when the single scopedness restriction is lifted (two |
1544 overlapping permutations) |
1570 overlapping permutations) |
1545 |
1571 |
|
1572 Future work: distinct list abstraction |
|
1573 |
|
1574 TODO: function definitions: |
|
1575 |
1546 |
1576 |
1547 The formalisation presented here will eventually become part of the |
1577 The formalisation presented here will eventually become part of the |
1548 Isabelle distribution, but for the moment it can be downloaded from |
1578 Isabelle distribution, but for the moment it can be downloaded from |
1549 the Mercurial repository linked at |
1579 the Mercurial repository linked at |
1550 \href{http://isabelle.in.tum.de/nominal/download} |
1580 \href{http://isabelle.in.tum.de/nominal/download} |
1551 {http://isabelle.in.tum.de/nominal/download}.\medskip |
1581 {http://isabelle.in.tum.de/nominal/download}.\medskip |
1552 *} |
1582 *} |
1553 |
1583 |
1554 text {* |
1584 text {* |
1555 |
|
1556 TODO: function definitions: |
|
1557 \medskip |
|
1558 |
|
1559 \noindent |
1585 \noindent |
1560 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1586 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1561 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1587 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1562 making the informal notes \cite{SewellBestiary} available to us and |
1588 making the informal notes \cite{SewellBestiary} available to us and |
1563 also for patiently explaining some of the finer points about the abstract |
1589 also for patiently explaining some of the finer points about the abstract |
1564 definitions and about the implementation of the Ott-tool. We |
1590 definitions and about the implementation of the Ott-tool. We |
1565 also thank Stephanie Weirich for suggesting to separate the subgrammars |
1591 also thank Stephanie Weirich for suggesting to separate the subgrammars |
1566 of kinds and types in our Core-Haskell example. |
1592 of kinds and types in our Core-Haskell example. |
1567 |
1593 |
1568 Lookup: Merlin paper by James Cheney; Mark Shinwell PhD |
1594 |
1569 |
|
1570 Future work: distinct list abstraction |
|
1571 |
1595 |
1572 |
1596 |
1573 *} |
1597 *} |
1574 |
1598 |
1575 |
1599 |