Posts By: Matthieu Sozeau
| Date | Post | Topic |
| 07/06/2010 | The connection with Noam Zeilberger's work... | An intuitionistic logic that proves Markov's principle |
| 03/22/2010 | Another take? | On the (Alleged) Value of Proof for Assurance |
| 04/23/2009 | Dependent type theories and LCF | The deBrujin Criterion and the "LCF Approach". |
| 01/16/2009 | A few reasons | On the Strength of Proof-Irrelevant Type Theories |
| 12/31/2008 | Inhabited | "Determinism" of types? |
| 12/26/2008 | Phase distinctions | The Lambda Cube & Some Programming Languages |
| 12/16/2008 | Refinement types | Any problems with true union types if all values are tagged? (like in a dynamically typed system, Lisp, etc.) |
| 11/29/2008 | Synchronous dataflow programming | Functional building blocks as concurrency patterns |
| 01/07/2009 | HOL | Non-standard type theories for FP |
| 02/11/2009 | Nope | Microsoft PDC "Language" Talks |
| 02/11/2009 | Misunderstanding | Microsoft PDC "Language" Talks |
| 02/11/2009 | Precisely | Microsoft PDC "Language" Talks |
| 11/12/2008 | Different inference problems | Subtyping + overloading |
| 11/12/2008 | I don't see what's weird here. | Subtyping + overloading |
| 11/23/2008 | Semantics | Subtyping + overloading |
| 11/08/2008 | Dependently typed languages | Question concerning parameterization over literals |
| 11/01/2008 | This has to do with Goedel | Total functional language self interpreter? |
| 11/01/2008 | An overgeneralization | Total functional language self interpreter? |
| 11/04/2008 | I stand corrected | Total functional language self interpreter? |
| 11/19/2008 | Which example? | Total functional language self interpreter? |
| 10/26/2008 | Why is there no proper dependent pattern-matching in Coq | Summary of Dependently Typed Systems? |
| 10/19/2008 | My guess | F in System F |
| 09/28/2008 | Modelling probabilistic programs | Workshop on Probabilistic Programming in December |
| 07/28/2008 | As another functor | Type classes and type generator restrictions |
| 04/17/2008 | Hope this helps | Breaking region nesting in type-and-effect systems? |
| 04/16/2008 | Refinement | Algebra of programming using dependent types |
| 04/03/2008 | Two problems | Rewriting rules for deducing properties of functions |
| 04/04/2008 | Not too hard.. to be useful | Rewriting rules for deducing properties of functions |
| 07/22/2008 | Lucid interpreter | Is null needed? |
| 02/10/2008 | Same with typeclasses instead of modules | Lanugages with built-in rules/tests? |
| 02/10/2008 | Classes and modules | Lanugages with built-in rules/tests? |
| 01/30/2008 | Subtyping | The YNot Project |
| 01/23/2008 | Type-safe printf using delimited continuations, in Coq | Type-safe printf using delimited continuations, in Coq |
| 01/23/2008 | Russell status | Type-safe printf using delimited continuations, in Coq |
| 01/24/2008 | Coq version | Type-safe printf using delimited continuations, in Coq |
| 01/24/2008 | soon is... | Type-safe printf using delimited continuations, in Coq |
| 01/22/2008 | Getting rid of the natural | Induction of variadic functions, functions over tuples, etc. |
| 01/22/2008 | Getting rid of the natural | Induction of variadic functions, functions over tuples, etc. |
| 09/13/2007 | Refinement | Extending HM type inference -- would this be possible? Or even desirable? |
| 07/09/2007 | Strong Normalization is a bliss | Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus) |
| 07/10/2007 | Practical matters | Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus) |
| 07/10/2007 | Sized types to the rescue | Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus) |
| 04/20/2007 | Type theory vs Set theory | Why is there not a PL with a mathematical type system? |
| 04/21/2007 | PVS and Coq | Why is there not a PL with a mathematical type system? |
| 04/21/2007 | What's reality ? | Why is there not a PL with a mathematical type system? |
| 04/22/2007 | Which Telescopes ? | Why is there not a PL with a mathematical type system? |
| 09/26/2008 | Coq documentation and proof management support | Course on Interactive Computer Theorem Proving Based on Coq |
| 03/22/2007 | Elegant Programming Languages | A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language |
| 03/23/2007 | Yes it is when you want certification. | A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language |
| 03/22/2007 | Typed tactics | A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language |
| 03/13/2007 | Duality with extraction | Concoqtion: Indexed Types Now! |
| 02/22/2007 | Inaccessible | Using Category Theory to Design Implicit Conversions and Generic Operators |
| 02/24/2007 | Commutation proof | Using Category Theory to Design Implicit Conversions and Generic Operators |
| 09/16/2008 | Just do it! | Typing a function which includes its axioms? |
| 06/25/2006 | Epigram/DML/ATS/Coq | Applied Type System vs. Epigram |
| LtU Topic Index Sorted by Date | LtU Topic Index Sorted by Topic | LtU Index of Post Authors | Zipped LtU Archive |