[TYPES] Writing syntactic models with "full information"

[Ambrus Kaposi]

On Mon, May 23, 2022 at 9:52 PM Stefan Monnier <monnier at 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$