Hume (Higher-order Unified Meta-Environment) is a strongly typed, mostly-functional language with an integrated tool set for developing, proving and assessing concurrent, safety-critical systems. Hume aims to extend the frontiers of language design for resource-limited systems, including real-time embedded and safety-critical systems, by introducing new levels of abstraction and provability.
I am a postdoctoral research fellow, interested in type theory, dependently typed functional programming, multi-stage programming, compilers and programming language design. I am now working on the Generative Programming for Embedded Systems project, in the context of the Hume programming language. Software * Idris, an experimental language with full dependent types. * Ivor, a type theory based theorem proving engine with a Haskell API. * A Supercombinator Compiler, intended as a back end for Epigram. Some other toys: * A simple functional language with a built-in theorem prover, implemented with the help of Ivor. * An implementation of the simply typed lambda calculus in Ivor, with a Haskell driver. * An SK calculus evaluator, being a small experiment in modelling partial functions in Coq.
"Welcome to the home page of davidhume.org, a site devoted to the works of, and scholarship about, the great philosopher David Hume (1711-1776). The site was created, and is administered, by Dr Peter Millican, Fellow and Tutor in Philosophy at Hertford College, Oxford University, and currently Co-Editor of the journal Hume Studies, and Amyas Merivale, part time Research Officer at the Leeds Electronic Text Centre and part time PhD student at Leeds University (working on Hume’s Four Dissertations). The site is under development, and Hume scholars with potential contributions or suggestions are invited to send them to peter@davidhume.org"