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
Name Binding Admin wrote 1 month 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
Name Binding Admin wrote 1 month ago: By Ulrich Schopp and Ian Stark, from CSL 2004, available from Ian Stark’s website: We consider … more →
Resource aware DSELs
edwinb wrote 9 months ago: Just wrote a short note about implementing resource aware domain specific languages by embedding in … more →
FP@StAnd
edwinb wrote 9 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
edwinb 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
edwinb 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
edwinb 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
edwinb 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
edwinb 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
edwinb wrote 2 years ago: I’m working on Ivor, a theorem proving library for Haskell. It’s an implementation of de … more →
