← All problems
Unverified

Expansion Postponement for Pure Type Systems

Replace the usual conversion rule of a Pure Type System by separate contraction and expansion rules. Expansion Postponement is the assertion that every derivable judgement has a derivation using the expansion rule at most once, and then only as the final inference. Does Expansion Postponement hold for every Pure Type System?

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu