Philip Wadler

icon indicating a website link http://homepages.inf.ed.ac.uk/wadler/ icon indicating an email [email protected]

icon company University of Edinburgh icon location Edinburgh icon location Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK.

Results 4 issues of Philip Wadler

Long arrows should be a multiple of monospace

6 comment

Currently, long arrows (⟵ ⟸ ⟶ ⟹) have a length about 11/12 of the monospaced characters. For laying out code (e.g., in Agda) it would be extremely helpful if their...

enhancement

Bug in appendix Substitution

1 comment

Section [The σ algebra equations](https://plfa.inf.ed.ac.uk/Substitution/#the-%CF%83-algebra-equations) contains the equation (sub-abs) ⟪ σ ⟫ (ƛ N) ≡ ƛ ⟪ σ ⟫ N This is wrong, as is the subsequent discussion ("The equations...

Tspl 2024 10 11

Previous version forgot to update 2024/tspl.md.

PLFA 2025 10 27: change how `eval` is defined

4 comment

Following a suggestion of Conrad Watt, changed the definition of `eval` to add information. Recall that the evaluator takes an amount of gas and a term and returns a reduction...