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 and alone?

References for # 4

Problem # 5

Submitted by Paweł Urzyczyn

Statement. Are there terms untypable in 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 collapse on ?

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 , determine the set of terms which can be typed in the stratiﬁed polymorphic type assignment system of order .

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 ?

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

[Next] [Previous] [Up]

Last modified: July 21, 2014