Go to the corresponding LIPIcs Volume Portal |
Felicissimo, Thiago ; Blanqui, Frédéric ; Barnawal, Ashish Kumar
pdf-format: |
|
@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19, author = {Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar}, title = {{Translating Proofs from an Impredicative Type System to a Predicative One}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {19:1--19:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17480}, URN = {urn:nbn:de:0030-drops-174801}, doi = {10.4230/LIPIcs.CSL.2023.19}, annote = {Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti} }
Keywords: | Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti | |
Collection: | 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) | |
Issue Date: | 2023 | |
Date of publication: | 01.02.2023 | |
Supplementary Material: | Software (Source Code): https://github.com/Deducteam/predicativize archived at: https://archive.softwareheritage.org/swh:1:dir:b2a1f99fe459c3e9a30debb4285eda1419b5d52d |