We provide a paradigmatic case study, about the formalization of System F<:'s type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F<:'s metatheory, on the other hand we address the equivalence of the two approaches internally to Coq.

Mechanizing type environments in weak HOAS

CIAFFAGLIONE, Alberto;SCAGNETTO, Ivan
2015

Abstract

We provide a paradigmatic case study, about the formalization of System F<:'s type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F<:'s metatheory, on the other hand we address the equivalence of the two approaches internally to Coq.
File in questo prodotto:
File Dimensione Formato  
tcs-14-revision2.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Non pubblico
Dimensione 434.81 kB
Formato Adobe PDF
434.81 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1-s2.0-S0304397515006404-main.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 595.33 kB
Formato Adobe PDF
595.33 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
tcs-14.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Pre-print
Licenza: Creative commons
Dimensione 384.15 kB
Formato Adobe PDF
384.15 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1072580
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact