School of Computing

Apr 6
15:00 - 15:40
PLAS: CO620: Declan Barnes
PLAS Group Seminar
Pattern matching Modulo Theories in Granule

This project looks to improve the pattern matching facilities of the Granule programming language, particularly by making use of an SMT solver. We develop a method for case splitting which generates potential patterns for a set of of variables. This functionality is inspired by the Agda language and uses the same syntax, though the SMT solver allows splitting to succeed in cases where Agda's unification fails. This functionality is complemented by an automatic rewriting system which transforms source files containing holes.We also develop an algorithm for propagating theorems from failed pattern matches to the relevant parts of later patterns, this gives the SMT solver more information when evaluating a pattern's validity, allowing it to accept well-typed definitions which would be rejected if the pattern was considered in isolation.


United Kingdom


Contact: O.Chitil
School of Computing

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 14/08/2015