types-list  

Messages by Thread

• Re: [TYPES] Types-list Digest, Vol 121, Issue 4 jan Vitek
  • Re: [TYPES] Types-list Digest, Vol 121, Issue 4 Andrew Myers
• [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Gabriel Scherer
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Jonathan Aldrich
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Tim Sweeney
  • Re: [TYPES] In a letter to the US White House, selinger
  • Re: [TYPES] In a letter to the US White House, Robert Rand
  • Re: [TYPES] In a letter to the US White House, Gabriel Scherer
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Stefan Monnier
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Rishiyur Nikhil
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Roberto Di Cosmo
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Gabriel Scherer
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Andrew Myers
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Gabriel Scherer
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Andrew Myers
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Tadeusz Litak
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Derek Dreyer
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Cristina Videira Lopes
  • Re: [TYPES] In a letter to the US White House, ACM opposes free distribution of peer-reviewed journal articles Stefan Monnier
• [TYPES] Summary of tricks for setting figures of rules in LaTeX Norman Ramsey
• [TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules Norman Ramsey
  • Re: [TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules Elias Castegren
  • Re: [TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules Peter Sewell
  • Re: [TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules Gabriel Scherer
  • Re: [TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules Filip Sieczkowski
  • Re: [TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules William J. Bowman
• [TYPES] Example uses of impredicativity Stefan Monnier
  • Re: [TYPES] Example uses of impredicativity William J. Bowman
  • Re: [TYPES] Example uses of impredicativity Martin Escardo
  • Re: [TYPES] Example uses of impredicativity Matthieu Sozeau
  • Re: [TYPES] Example uses of impredicativity Benjamin C. Pierce
  • Re: [TYPES] Example uses of impredicativity Beta Ziliani
• [TYPES] An order-theoretic approach to OO generics moez
  • Re: [TYPES] An order-theoretic approach to OO generics moez
• [TYPES] Theory of Particular Sets Paul Blain Levy
• [TYPES] Variants and [Park or Scott] fixpoint Induction O'Hearn, Peter
  • Re: [TYPES] Variants and [Park or Scott] fixpoint Induction Sergey Goncharov
  • Re: [TYPES] Variants and [Park or Scott] fixpoint Induction Tadeusz Litak
  • Re: [TYPES] Variants and [Park or Scott] fixpoint Induction Thomas Streicher
  • Re: [TYPES] Variants and [Park or Scott] fixpoint Induction O'Hearn, Peter
  • Re: [TYPES] Variants and [Park or Scott] fixpoint Induction Ben Sherman
• [TYPES] What exactly should we call syntax-directed inference rules? Julia Belyakova
  • Re: [TYPES] What exactly should we call syntax-directed inference rules? Frank Pfenning
  • Re: [TYPES] What exactly should we call syntax-directed inference rules? Julia Belyakova
  • Re: [TYPES] What exactly should we call syntax-directed inference rules? Frank Pfenning
  • Re: [TYPES] What exactly should we call syntax-directed inference rules? Julia Belyakova
• [TYPES] Why cannot declare a super type dynamically? Xuhui Li
  • Re: [TYPES] Why cannot declare a super type dynamically? Jeremy Siek
  • Re: [TYPES] Why cannot declare a super type dynamically? Marco Servetto
• [TYPES] How to code interesting examples in λC Beta Ziliani
  • Re: [TYPES] How to code interesting examples in λC Herman Geuvers
  • Re: [TYPES] How to code interesting examples in λC Beta Ziliani
• [TYPES] Order of evaluation rules in untyped lambda-calculus Brian Berns
  • Re: [TYPES] Order of evaluation rules in untyped lambda-calculus John Clements
  • Re: [TYPES] Order of evaluation rules in untyped lambda-calculus Brian Berns
  • Re: [TYPES] Order of evaluation rules in untyped lambda-calculus John Clements
  • Re: [TYPES] Order of evaluation rules in untyped lambda-calculus Brian Berns
  • Re: [TYPES] Order of evaluation rules in untyped lambda-calculus Ezra e. k. Cooper
• [TYPES] Conversion irrelevance and extensionality Stefan Monnier
• [TYPES] Gödel's T extended with an eta-like rule for the recursor Ansten Mørch Klev
  • Re: [TYPES] Gödel's T extended with an eta-like rule for the recursor Frédéric Blanqui
  • Re: [TYPES] ?==?utf-8?q? ?==?utf-8?q? Gödel's T extended with an eta-like rule for the recursor Sergei Soloviev
  • Re: [TYPES] Gödel's T extended with an eta-like rule for the recursor David CHEMOUIL
  • Re: [TYPES] Gödel's T extended with an eta-like rule for the recursor Danel Ahman
  • Re: [TYPES] Gödel's T extended with an eta-like rule for the recursor Danko ILIK
• [TYPES] Literature relating subtyping to positivity checking for recursive types? Christopher Jenkins
  • Re: [TYPES] Literature relating subtyping to positivity checking for recursive types? Gabriel Scherer
  • Re: [TYPES] Literature relating subtyping to positivity checking for recursive types? Sandro Stucki
  • Re: [TYPES] Literature relating subtyping to positivity checking for recursive types? Christopher Jenkins
  • Re: [TYPES] Literature relating subtyping to positivity checking for recursive types? Christopher Jenkins
• [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction Ahmed Bhayat
  • Re: [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction James Koppel
  • Re: [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction Frédéric Blanqui
  • Re: [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction Damiano Mazza
  • Re: [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction Ahmed Bhayat
  • Re: [TYPES] Reduction ordering on terms of simply-typed lambda-calculus compatible with beta-reduction James Koppel
• [TYPES] Translation of bounded quantifications into intersection types Ningning Xie
  • Re: [TYPES] Translation of bounded quantifications into intersection types Ningning Xie
  • Re: [TYPES] Translation of bounded quantifications into intersection types Stephen Dolan
  • Re: [TYPES] Translation of bounded quantifications into intersection types Giuseppe Castagna
  • Re: [TYPES] Translation of bounded quantifications into intersection types Stephen Dolan
• [TYPES] type inference for mutually recursive algebraic types with subtyping Aaron Gray
  • Re: [TYPES] type inference for mutually recursive algebraic types with subtyping Sam Lindley
  • Re: [TYPES] type inference for mutually recursive algebraic types with subtyping Aaron Gray
  • Re: [TYPES] type inference for mutually recursive algebraic types with subtyping Rodolphe Lepigre
  • Re: [TYPES] type inference for mutually recursive algebraic types with subtyping Aaron Gray
  • Re: [TYPES] type inference for mutually recursive algebraic types with subtyping Giuseppe Castagna
• [TYPES] Interaction between type classes and modules Philip Wadler
  • Re: [TYPES] Interaction between type classes and modules Steven Shaw
  • Re: [TYPES] Interaction between type classes and modules Derek Dreyer
• [TYPES] Programming Language Foundations in Agda Philip Wadler
• [TYPES] Equi recursive types: logical relations and intuition Marco Patrignani
  • Re: [TYPES] Equi recursive types: logical relations and intuition Gabriel Scherer
  • Re: [TYPES] Equi recursive types: logical relations and intuition Paolo Giarrusso
  • Re: [TYPES] Equi recursive types: logical relations and intuition Marco Patrignani
  • Re: [TYPES] Equi recursive types: logical relations and intuition Guy McCusker
• [TYPES] "Proofs of life" Rene Vestergaard
  • Re: [TYPES] "Proofs of life" Rene Vestergaard
• [TYPES] Do erasable boxes form a monad? Stefan Monnier
  • Re: [TYPES] Do erasable boxes form a monad? Jesper Cockx
  • Re: [TYPES] Do erasable boxes form a monad? Stefan Monnier
• [TYPES] Martin Hofmann memorial talk Benjamin C. Pierce
• [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics Jeremy Siek
  • Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics Gabriel Scherer
  • Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics William J. Bowman
  • Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics Jeremy Siek
  • Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics Gabriel Scherer
  • Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics Jeremy Siek
  • Re: [TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics Neel Krishnaswami
• [TYPES] models of untyped lambda calculus Rosu, Grigore
  • Re: [TYPES] models of untyped lambda calculus Rosu, Grigore
  • Re: [TYPES] models of untyped lambda calculus Gabriel Scherer
  • Re: [TYPES] models of untyped lambda calculus Albert R Meyer
  • Re: [TYPES] models of untyped lambda calculus Gabriel Scherer
• [TYPES] Max on terminology: "Graduality" instead of "Gradual Guarantee" Gabriel Scherer
• [TYPES] Transfinite universe levels Stefan Monnier
  • Re: [TYPES] Transfinite universe levels Erik Palmgren
  • Re: [TYPES] Transfinite universe levels Dan Doel
  • Re: [TYPES] Transfinite universe levels Philippa Cowderoy
  • Re: [TYPES] Transfinite universe levels Gabriel Scherer
• [TYPES] What is the state of the art of call-by-value computing? Roman
  • Re: [TYPES] What is the state of the art of call-by-value computing? Frédéric Blanqui
  • Re: [TYPES] What is the state of the art of call-by-value computing? Roman
• [TYPES] Progress + Preservation = Evaluation Philip Wadler
  • Re: [TYPES] Progress + Preservation = Evaluation William J. Bowman
  • Re: [TYPES] Progress + Preservation = Evaluation Philip Wadler
  • Re: [TYPES] Progress + Preservation = Evaluation Oleg
  • Re: [TYPES] Progress + Preservation = Evaluation Philip Wadler
  • Re: [TYPES] Progress + Preservation = Evaluation Pierre Courtieu
  • Re: [TYPES] Progress + Preservation = Evaluation Philip Wadler
  • Re: [TYPES] Progress + Preservation = Evaluation Sam Lindley
  • Re: [TYPES] Progress + Preservation = Evaluation Philip Wadler
  • Re: [TYPES] [Agda] Progress + Preservation = Evaluation Roman
• [TYPES] meta thread on types-announces filtering of announces Gabriel Scherer
• [TYPES] Decidable equality of propositions implies proof irrelevance Dominik Kirst
• [TYPES] Generalised Covariant and Contravariant inference rules Aaron Gray
• [TYPES] System F and System T names Alejandro Díaz-Caro
  • Re: [TYPES] System F and System T names Neel Krishnaswami
  • Re: [TYPES] System F and System T names Alejandro Díaz-Caro
• [TYPES] breaking abstraction with ML exceptions Sam Lindley
  • Re: [TYPES] breaking abstraction with ML exceptions Gabriel Scherer
  • Re: [TYPES] breaking abstraction with ML exceptions Oleg
  • Re: [TYPES] breaking abstraction with ML exceptions Derek Dreyer
  • Re: [TYPES] breaking abstraction with ML exceptions Sam Lindley
  • Re: [TYPES] breaking abstraction with ML exceptions François Pottier
  • Re: [TYPES] breaking abstraction with ML exceptions Andrew Myers
• [TYPES] What algebra am I thinking of? Philip Wadler
  • Re: [TYPES] What algebra am I thinking of? Matthew Meola
  • Re: [TYPES] What algebra am I thinking of? Radu Grigore
  • Re: [TYPES] What algebra am I thinking of? Eugenio Moggi
  • Re: [TYPES] What algebra am I thinking of? Harrison Brown
  • Re: [TYPES] What algebra am I thinking of? Jacques Carette
  • Re: [TYPES] What algebra am I thinking of? Philip Wadler
  • Re: [TYPES] What algebra am I thinking of? Neel Krishnaswami
  • Re: [TYPES] What algebra am I thinking of? Jacques Carette
  • Re: [TYPES] What algebra am I thinking of? Philip Wadler
  • Re: [TYPES] What algebra am I thinking of? Neel Krishnaswami
  • Re: [TYPES] What algebra am I thinking of? Tadeusz Litak
  • Re: [TYPES] What algebra am I thinking of? Francesco Gavazzo
  • Re: [TYPES] What algebra am I thinking of? Philip Wadler
  • Re: [TYPES] What algebra am I thinking of? Tadeusz Litak
  • Re: [TYPES] What algebra am I thinking of? Peter Selinger
  • Re: [TYPES] What algebra am I thinking of? Valeria de Paiva
• [TYPES] Existing Work on Function Destructors or Haskell Type Spec? Zachary Palmer
  • Re: [TYPES] Existing Work on Function Destructors or Haskell Type Spec? Filippo Sestini
  • Re: [TYPES] Existing Work on Function Destructors or Haskell Type Spec? Richard Eisenberg
  • Re: [TYPES] Existing Work on Function Destructors or Haskell Type Spec? Neel Krishnaswami
  • Re: [TYPES] Existing Work on Function Destructors or Haskell Type Spec? matthias
  • Re: [TYPES] Existing Work on Function Destructors or Haskell Type Spec? Philip Wadler
• [TYPES] A new take on bracket abstraction, and a historical question about the first take Oleg
  • Re: [TYPES] A new take on bracket abstraction, and a historical question about the first take Gabriel Scherer
• [TYPES] Typed lambda calculi with weak conversion Filippo Sestini
  • Re: [TYPES] Typed lambda calculi with weak conversion Gabriel Scherer
  • Re: [TYPES] Typed lambda calculi with weak conversion Thibaut Balabonski
  • Re: [TYPES] Typed lambda calculi with weak conversion Filippo Sestini
  • Re: [TYPES] Typed lambda calculi with weak conversion Thorsten Altenkirch
• [TYPES] Best pedagogical presentation of CPS? Benjamin C. Pierce
  • Re: [TYPES] Best pedagogical presentation of CPS? François Pottier
  • Re: [TYPES] Best pedagogical presentation of CPS? Xavier Leroy
  • Re: [TYPES] Best pedagogical presentation of CPS? Philip Wadler
  • Re: [TYPES] Best pedagogical presentation of CPS? Adam Chlipala
  • Re: [TYPES] Best pedagogical presentation of CPS? Paul Blain Levy
  • Re: [TYPES] Best pedagogical presentation of CPS? Yuting Wang
• [TYPES] Martin Hofmann (1965-2018) Jan Hoffmann
  • Re: [TYPES] Martin Hofmann (1965-2018) Eijiro Sumii
• [TYPES] preterms Stefan Ciobaca
  • Re: [TYPES] preterms Jay Sulzberger
  • Re: [TYPES] preterms Jay Sulzberger
• [TYPES] Objects in type theory Tim Sweeney
  • Re: [TYPES] Objects in type theory Nicolai Kraus
  • Re: [TYPES] Objects in type theory Kim Bruce
• [TYPES] Statement of structural induction Richard Eisenberg
  • Re: [TYPES] Statement of structural induction Burak Emir
  • Re: [TYPES] Statement of structural induction Ben Sherman
  • Re: [TYPES] Statement of structural induction James Wood
  • Re: [TYPES] Statement of structural induction Xavier Leroy
  • Re: [TYPES] Statement of structural induction Albert R Meyer
  • Re: [TYPES] Statement of structural induction Xavier Leroy
  • Re: [TYPES] Statement of structural induction Frédéric Blanqui
  • Re: [TYPES] Statement of structural induction Paolo Giarrusso

• Earlier messages
• Later messages