Posts tagged "types"
-
Two Different Flavors of Type Theory - September 27, 2015
-
Type is not in Type - August 26, 2015
-
Solving Recursive Equations - August 14, 2015
-
Learn Type Theory - August 14, 2015
-
A Basic Tutorial on JonPRL - July 6, 2015
-
Proving Cut Admissibility in Twelf - June 29, 2015
-
A Proof of Church Rosser in Twelf - May 5, 2015
-
Bracket Abstraction: The Smallest PL You've Ever Seen - May 1, 2015
-
A Tiny Compiler For A Typed Higher Order Language - March 24, 2015
-
Worlds in Twelf - March 7, 2015
-
An Explanation of Type Inference for ML/Haskell - February 28, 2015
-
A Twelf Introduction - February 28, 2015
-
Notes on Proof Theory: Part 1 - February 11, 2015
-
Observations about -XStaticPointers - January 27, 2015
-
Why Constructive Logic - January 9, 2015
-
What Are Impredicative Types? - December 23, 2014
-
Notes on Parametricity - December 22, 2014
-
Treating Programs like Vending Machines - December 19, 2014
-
Bidirectional Type Checkers for λ→ and λΠ - November 22, 2014
-
Notes on Focusing - October 27, 2014
-
Notes on Quotients Types - October 17, 2014
-
Notes on Abstract and Existential Types - September 29, 2014
-
Introduction to Dependent Types: Off, Off to Agda Land - September 21, 2014
-
Introduction to Dependent Types: Haskell on Steroids - August 25, 2014
-
Equality is Hard - August 6, 2014
-
Many Shades of Halting Oracles - July 30, 2014
-
A Tutorial on Church Representations - July 19, 2014
-
Dissecting crush - July 9, 2014
-
Some Useful Agda - June 28, 2014
-
Church Representations: Part 3 - March 10, 2014
-
Church Representations: Part 2 - March 7, 2014
-
Church Representations - March 6, 2014
-
Types and Kinds and Sorts, Oh My! - February 10, 2014
-
Faking Existentials with Rank N Types - January 14, 2014
-
Some Fun Dependently Typed Programs - December 24, 2013
-
Fixpoints and Iso-recursive Types - November 9, 2013
-
forall Means All! - October 6, 2013