Lambda the Ultimate

I'm an undergrad at The University of Alabama in Huntsville, which, unfortunately, has a subpar Computer Science program, so I'm learning independently from whatever papers I can find on the Internet.

I'm particularly interested in dependent types and provable programming, and my (overly-) ambitious hope is to apply such a sound type system to a new language and operating system kernel combination.