Problem Anthology

Problem # 1 [SOLVED]
  Submitted by Roger Hindley
  Statement. Is there a direct proof of the conﬂuence of $β η$ -strong reduction?
  References for # 1

Problem # 2 [SOLVED]
  Submitted by Roger Hindley
  Statement. Is ticket entailment decidable?
  References for # 2

Problem # 3 [SOLVED]
  Submitted by Richard Statman
  Statement. Does the range property hold for the theory $ℋ$ ?
  References for # 3

Problem # 4
  Submitted by Richard Statman
  Statement. A ﬁxed point combinator from $B$ and $ω$ alone?
  References for # 4

Problem # 5
  Submitted by Paweł Urzyczyn
  Statement. Are there terms untypable in $F ω$ but typable with help of positive recursive types?
  References for # 5

Problem # 6
  Submitted by Richard Statman
  Statement. Basis Decision Problem.
  References for # 6

Problem # 7
  Submitted by Richard Statman
  Statement. Word problem for combinators of orders less than 3.
  References for # 7

Problem # 8
  Submitted by Richard Statman
  Statement. Which results on one-step effective strategies carry over from combinatory logic to lambda-calculus?
  References for # 8

Problem # 9
  Submitted by Morten Heine Sørensen
  Statement. Is every weakly normalizing PTS also strongly normalizing?
  References for # 9

Problem # 10
  Submitted by Richard Statman
  Statement. Do uniform universal generators exist?
  References for # 10

Problem # 11
  Submitted by Paweł Urzyczyn
  Statement. Which equations on intersection types preserve normalization?
  References for # 11

Problem # 12
  Submitted by Paweł Urzyczyn
  Statement. Does the typability hierarchy of $Fω$ collapse on $F1$ ?
  References for # 12

Problem # 13
  Submitted by Mariangiola Dezani-Ciancaglini
  Statement. Inhabitation for intersection type systems
  References for # 13

Problem # 14
  Submitted by Simona Ronchi Della Rocca
  Statement. For every $n$ , determine the set of terms which can be typed in the stratiﬁed polymorphic type assignment system of order $n$ .
  References for # 14

Problem # 15
  Submitted by Alex Simpson
  Statement. Is the equational theory of typed $λ$ -calculus with ﬁnite sums the maximum consistent typically-ambiguous congruence?
  References for # 15

Problem # 16
  Submitted by Jakob Rehof
  Statement. Is the subtype entailment problem decidable?
  References for # 16

Problem # 17
  Submitted by Paweł Urzyczyn
  Statement. Can recursive types be deﬁned in system $F$ ?
  References for # 17

Problem # 18
  Submitted by Mariangiola Dezani-Ciancaglini
  Statement. Find trees representing contextual equivalences
  References for # 18

Problem # 19 [SOLVED]
  Submitted by Mariangiola Dezani-Ciancaglini
  Statement. Does easiness imply simple easiness?
  References for # 19

Problem # 20 [SOLVED]
  Submitted by Mariangiola Dezani-Ciancaglini
  Statement. Type theoretic characterisation of hereditary permutations
  References for # 20

Problem # 21
  Submitted by Paweł Urzyczyn
  Statement. Is higher-order matching decidable with many atoms?
  References for # 21

Problem # 22
  Submitted by Furio Honsell
  Statement. Is there a continuously complete CPO model of the $λ$ -calculus whose theory is precisely $λβη$ or $λβ$ ?
  References for # 22

Problem # 23
  Submitted by Robin Adams
  Statement. Does Expansion Postponement hold for every PTS?
  References for # 23

Problem # 24
  Submitted by Corrado Böhm
  Statement. On the equational meaning of deeds
  References for # 24

Problem # 25
  Submitted by Benedetto Intrigila
  Statement. How many ﬁxed points can a combinator have?
  References for # 25

Problem # 26
  Submitted by Henk Barendregt
  Statement. Assign (in an ‘easy’ way) ordinals to terms of the simply typed lambda calculus such that reduction of the term yields a smaller ordinal.
  References for # 26