[Next]  [Previous]  [Up]  

Problem Anthology

A full version of the TLCA List of Open Problems can be downloaded HERE . Moreover, a two pages per sheet can be downloaded from HERE .

  Problem # 1 [SOLVED]
  Submitted by Roger Hindley
  Statement. Is there a direct proof of the confluence 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 fixed 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 stratified 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 finite 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 defined 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 fixed 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

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014