Blogs about: Dependent Types
Featured Blog
Resource aware DSELs
Just wrote a short note about implementing resource aware domain specific languages by embedding in Idris. Still much to do, but the notation is getting better (less need to write strange looking type… more →
Types, Programming, etc.
Practical programming with higher-order encodings and dependent types
wrote 2 months ago: By Adam Poswolsky and Carsten Schurmann, from ESOP 2008, available from the Delphin website: Higher- … more →
A dependent type theory with names and binding
wrote 2 months ago: By Ulrich Schopp and Ian Stark, from CSL 2004, available from Ian Stark’s website: We consider … more →
Resource aware DSELs
wrote 10 months ago: Just wrote a short note about implementing resource aware domain specific languages by embedding in … more →
FP@StAnd
wrote 10 months ago: We’ve finally gone all Web 2.0 in the Functional Programming group at St Andrews. Lots of us a … more →
Correct-by-construction Concurrency
— 1 comment
wrote 1 year ago: I’ve been hacking merrily away in Idris over the last couple of weeks, seeing what I can make … more →
Idris, a language with dependent types
— 3 comments
wrote 1 year ago: I was at the Dependently Typed Programming ‘08 workshop a couple of weeks ago, and it was a lo … more →
Silence, and adding things up
wrote 2 years ago: Well, so much for new year resolutions . I’d like to claim I haven’t posted anything for … more →
Stack machines
— 2 comments
wrote 2 years ago: Back in the time before at Durham, we had a snazzy whiteboard on which you could press a button and … more →
Correctness by Construction - a Carry-Ripple Adder
wrote 2 years ago: I dedided to to try out Ivor’s new pattern matching gadgetry by implementing a program I … more →
Dependent Pattern Matching in Ivor
wrote 2 years ago: I’m working on Ivor, a theorem proving library for Haskell. It’s an implementation of de … more →
