Text this: An integration of reduction and logic for programming languages