User:DPMulligan: Difference between revisions
Content deleted Content added
DPMulligan (talk | contribs) No edit summary |
DPMulligan (talk | contribs) No edit summary |
||
| Line 1: | Line 1: | ||
I'm a [[PhD]] student in [[theoretical computer science]] in the Dependable Systems Group, Heriot-Watt University, Edinburgh, where I work with [[nominal techniques]], specifically, various interesting extensions of [[nominal terms]]. My academic interests are [[mathematics]], [[logic]] and [[computer science]]. |
I'm a [[PhD]] student in [[theoretical computer science]] in the Dependable Systems Group, Heriot-Watt University, Edinburgh, where I work with [[nominal techniques]], specifically, various interesting extensions of [[nominal terms]]. My academic interests are [[mathematics]], [[logic]] and [[computer science]]. |
||
My homepage is [http://www.macs.hw.ac.uk/~dpm8]. |
My homepage is [http://www.macs.hw.ac.uk/~dpm8]. I also run a blog on name binding (nominal techniques, [[higher-order abstract syntax]], [[de Bruijn indices]] etc.) [http://namebinding.wordpress.com]. |
||
I'm originally from [[Wigan]], [[Greater Manchester]], [[England]]. |
I'm originally from [[Wigan]], [[Greater Manchester]], [[England]]. |
||
Revision as of 13:33, 14 May 2010
I'm a PhD student in theoretical computer science in the Dependable Systems Group, Heriot-Watt University, Edinburgh, where I work with nominal techniques, specifically, various interesting extensions of nominal terms. My academic interests are mathematics, logic and computer science.
My homepage is [1]. I also run a blog on name binding (nominal techniques, higher-order abstract syntax, de Bruijn indices etc.) [2].
I'm originally from Wigan, Greater Manchester, England.
Pages started
- Rippling, meta-level heuristic guidance for inductive proof.
- IsaPlanner, a proof planning system for Isabelle.
- Nominal techniques, a group of related techniques for working with, and simplifying the reasoning about, languages with name binders.
- Nominal terms, a metalanguage for embedding object languages with name binding constructs into.
Pages I've made significant contributions to
- Lambda calculus, a formal system that internalises the notion of function
- Unification, the process of synthesising a substitution that identifies two input terms