[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Mon, May 23, 2022 at 9:52 PM Stefan Monnier <monn...@iro.umontreal.ca> wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Andreas Nuyts [2022-05-23 10:44:19] wrote: > > I would suggest the use of intrinsically typed syntax, defined as a quotient > > inductive-inductive type, see > > Altenkirch and Kaposi, Type theory in type theory using quotient inductive > > types > > https://urldefense.com/v3/__https://dl.acm.org/doi/abs/10.1145/2914770.2837638__;!!IBzWLUs!UJ6ZI5x-rdMfJBtHWEi-LWwQgG_CQHpnLN_7JsHtojjYqW_ixR1U0HB8byOCf9q-KWc6aS-u-n6vuFFt9h5QDz1rXwWOzGcVyw$ > > (and further work by either author). > > This way, omitting context and type is not cringe-worthy but formally > > justified in the sense that there is only a single (object-language) context > > and a single (object-language) type in which the (object-language) > > expression e is well-typed (in the metalanguage). > > I do tend to presume in my head that my terms are intrinsically typed, > which is why I'm tempted to play fast and loose and abuse notations with > things like [e] meaning [Γ ⊢ e : τ], but at the same time I'm not > completely comfortable relying on such a QIIT representation, because it > doesn't seem sufficiently well established yet. > > E.g. I've never seen this used in an article. Here is a random list of papers that use QIIT syntax. Some people call it "well-typed/intrinsic syntax quotiented by conversion" or "initial model/algebra of the language". Thorsten Altenkirch, Ambrus Kaposi: Normalisation by Evaluation for Type Theory, in Type Theory. Log. Methods Comput. Sci. 13(4) (2017) https://urldefense.com/v3/__https://doi.org/10.23638/LMCS-13(4:1)2017__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHXXcjFgk$ Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau: Setoid Type Theory - A Syntactic Translation. MPC 2019: 155-196 https://urldefense.com/v3/__https://doi.org/10.1007/978-3-030-33636-3_7__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHLET6tTc$ Thierry Coquand: Canonicity and normalization for dependent type theory. Theor. Comput. Sci. 777: 184-191 (2019) https://urldefense.com/v3/__https://doi.org/10.1016/j.tcs.2019.01.015__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatH_6H14yA$ Andreas Abel, Christian Sattler: Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus. PPDP 2019: 3:1-3:12 https://urldefense.com/v3/__https://doi.org/10.1145/3354166.3354168__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHNNF55NE$ András Kovács. Elaboration with first-class implicit function types. Proc. ACM Program. Lang. 4(ICFP): 101:1-101:29 (2020) https://urldefense.com/v3/__https://doi.org/10.1145/3408983__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHvgrE5ws$ Jonathan Sterling, Carlo Angiuli: Normalization for Cubical Type Theory. LICS 2021: 1-15 https://urldefense.com/v3/__https://doi.org/10.1109/LICS52264.2021.9470719__;!!IBzWLUs!RDvJg8Wh5lWFxZtFNvt0jkG968kLd1BJxx2Pu4Epfre8N1PRnKujIfjYYbJrmabdOK61SEgwmtf0yh3tB-wiqTXXHatHDJJWemc$
