### Skapa referens, olika format (klipp och klistra)

**Harvard**

Tuerk, T., Myreen, M. och Kumar, R. (2015) *Pattern matches in HOL: A new representation and improved code generation*.

** BibTeX **

@conference{

Tuerk2015,

author={Tuerk, Thomas and Myreen, Magnus O. and Kumar, Ramana},

title={Pattern matches in HOL: A new representation and improved code generation},

booktitle={Lecture Notes in Computer Science - Proceedings of the 6th International Conference on Interactive Theorem Proving, ITP 2015, Nanjing, China, 24-27 August 2015},

isbn={978-3-319-22101-4},

pages={453-468},

abstract={Pattern matching is ubiquitous in functional programming and also very useful for definitions in higher-order logic. However, it is not directly supported by higher-order logic. Therefore, the parsers of theorem provers like HOL4 and Isabelle/HOL contain a pattern-compilation algorithm. Internally, decision trees based on case constants are used. For non-trivial case expressions, there is a big discrepancy between the user’s view and the internal representation. This paper presents a new general-purpose representation for case expressions that mirrors the input syntax in the internal representation closely. Because of this close connection, the new representation is more intuitive and often much more compact. Complicated parsers and pretty printers are no longer required. Proofs can more closely follow the user’s intentions, and code generators can produce better code. Moreover, the new representation is more general than the currently used representation, supporting guards, patterns with multiple occurrences of the same bound variable, unbound variables, arithmetic expressions in patterns, and more. This work has been implemented in the HOL4 theorem prover and integrated into CakeML’s proof-producing code generator.},

year={2015},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 229817

A1 Tuerk, Thomas

A1 Myreen, Magnus O.

A1 Kumar, Ramana

T1 Pattern matches in HOL: A new representation and improved code generation

YR 2015

T2 Lecture Notes in Computer Science - Proceedings of the 6th International Conference on Interactive Theorem Proving, ITP 2015, Nanjing, China, 24-27 August 2015

SN 978-3-319-22101-4

SP 453

OP 468

AB Pattern matching is ubiquitous in functional programming and also very useful for definitions in higher-order logic. However, it is not directly supported by higher-order logic. Therefore, the parsers of theorem provers like HOL4 and Isabelle/HOL contain a pattern-compilation algorithm. Internally, decision trees based on case constants are used. For non-trivial case expressions, there is a big discrepancy between the user’s view and the internal representation. This paper presents a new general-purpose representation for case expressions that mirrors the input syntax in the internal representation closely. Because of this close connection, the new representation is more intuitive and often much more compact. Complicated parsers and pretty printers are no longer required. Proofs can more closely follow the user’s intentions, and code generators can produce better code. Moreover, the new representation is more general than the currently used representation, supporting guards, patterns with multiple occurrences of the same bound variable, unbound variables, arithmetic expressions in patterns, and more. This work has been implemented in the HOL4 theorem prover and integrated into CakeML’s proof-producing code generator.

LA eng

DO 10.1007/978-3-319-22102-1_30

LK http://dx.doi.org/10.1007/978-3-319-22102-1_30

OL 30