Gradual refinement blending pattern matching with data abstraction

Meng Wang, Jeremy Gibbons, Kazutaka Matsuda, Zhenjiang Hu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)


Pattern matching is advantageous for understanding and reasoning about function definitions, but it tends to tightly couple the interface and implementation of a datatype. Significant effort has been invested in tackling this loss of modularity; however, decoupling patterns from concrete representations while maintaining soundness of reasoning has been a challenge. Inspired by the development of invertible programming, we propose an approach to abstract datatypes based on a rightinvertible language rinv-every function has a right (or pre-) inverse.We show how this new design is able to permit a smooth incremental transition from programs with algebraic datatypes and pattern matching, to ones with proper encapsulation (implemented as abstract datatypes), while maintaining simple and sound reasoning.

Original languageEnglish
Title of host publicationMathematics of Program Construction - 10th International Conference, MPC 2010, Proceedings
Number of pages29
Publication statusPublished - 2010
Event10th International Conference on the Mathematics of Program Construction, MPC 2010 - Quebec City, QC, Canada
Duration: 2010 Jun 212010 Jun 23

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6120 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other10th International Conference on the Mathematics of Program Construction, MPC 2010
CityQuebec City, QC

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Gradual refinement blending pattern matching with data abstraction'. Together they form a unique fingerprint.

Cite this