coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Mechanised System F Omega

From: Elias Castegren <eliasca AT kth.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Mechanised System F Omega
Date: Fri, 15 Mar 2019 11:13:20 +0000
Accept-language: sv-SE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=eliasca AT kth.se; spf=Pass smtp.mailfrom=eliasca AT kth.se; spf=Pass smtp.helo=postmaster AT smtp-3.sys.kth.se
Ironport-phdr: 9a23:k8sY+h0BhS7rkkSEsmDT+DRfVm0co7zxezQtwd8Zse0XIvad9pjvdHbS+e9qxAeQG9mCs7Qc0qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHOfwlEniaxba5vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwjb5Urh2uqBFk347be4SVOOZicq/Bf94XQ3dKUMZLVyxGB4Oxd4QBD+4APelCtIn2ukUDogGlBQmwGuzvxSVIiWHw3aYn1OkuDwXG3A06ENIVrHvbts74NKQOUeC11qXI1ivMYupQ1Dzg64bIaggsreyCUL5sa8bd10ciGgHfglifqoHpJS6Z2+ATv2SD8uZtW/6jh3Q5pw1vpjWj3Nogh4fKi44Pzl3J9SN0y5svK9KiUk50e9ukHYNQty6EM4t2RdsvQ3ptuCYm0r0KoJC2cDIRyJUn3B7Tcf+Hc5SI4h75T+aePy90hHNjeL2hmxa/6VWsx+PgWsWuzlpHoChInsPDu30OzRDf98yKRuVl8kekwzmP1gTT6u9eIUAzkKrWM4AuwroxlpUJqkTMAjX5lV71jK+KdkUo4POo5Pr/brX8upCcL5N0ih35Mqk2hsO/Bv04PhESUGif5OSzz6bu/Vb5QbVPlv05iLPVsJHcJcQBp662GRVZ0og560X3MzDzmt8fhDwMKE9PUBOBlYngfV/UarisBvCmxl+ojT1DxvbcP7SnDI+bfVbZl7K0ULJ84lUU4wMo0d1Q/Z9SQuUMJPP6QUT4nN/EDlkiPlrnkK7cFNxh29ZGCiq0CaiDPfaK6A7a1qcUO+CJIbQtlnP4Ivkh6eTpiC9rmkMdO7Kkj8JONCKIW89+KkDcWkLCx88bGDdYvRY+Cvfn2gXbDGxjIk2qVqd53QkVTYKrCYCaF9K2haCZmXz9BYxNIGNaChaXHCWxeg==

Hi Coq Club

I have been looking for a Coq specification of System F Omega,
but have only found System F with variations which are not of the
computations-on-the-type-level kind. I have found mechanisations
of the Calculus of Constructions, but I’m not ready to go full on
dependent just yet =)

Does anyone know of a formulation of System F Omega in Coq?

Best

/Elias

[Coq-Club] Mechanised System F Omega, Elias Castegren, 03/15/2019