Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)
Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster. Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). In Dagstuhl Reports, Volume 11, Issue 10, pp. 151-172, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@Article{coquand_et_al:DagRep.11.10.151, author = {Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.}, title = {{Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)}}, pages = {151--172}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2022}, volume = {11}, number = {10}, editor = {Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.10.151}, URN = {urn:nbn:de:0030-drops-159321}, doi = {10.4230/DagRep.11.10.151}, annote = {Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 25:1-25:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{xu:LIPIcs.FSCD.2020.25, author = {Xu, Chuangjie}, title = {{A Gentzen-Style Monadic Translation of G\"{o}del’s System T}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {25:1--25:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.25}, URN = {urn:nbn:de:0030-drops-123472}, doi = {10.4230/LIPIcs.FSCD.2020.25}, annote = {Keywords: monadic translation, G\"{o}del’s System T, logical relation, negative translation, majorizability, continuity, bar recursion, Agda} }
Published in: Dagstuhl Seminar Proceedings, Volume 4351, Spatial Representation: Discrete vs. Continuous Computational Models (2005)
Douglas Bridges, Hajime Ishihara, Peter Schuster, and Luminita S. Vita. Compactness in apartness spaces?. In Spatial Representation: Discrete vs. Continuous Computational Models. Dagstuhl Seminar Proceedings, Volume 4351, pp. 1-7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)
@InProceedings{bridges_et_al:DagSemProc.04351.9, author = {Bridges, Douglas and Ishihara, Hajime and Schuster, Peter and Vita, Luminita S.}, title = {{Compactness in apartness spaces?}}, booktitle = {Spatial Representation: Discrete vs. Continuous Computational Models}, pages = {1--7}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2005}, volume = {4351}, editor = {Ralph Kopperman and Michael B. Smyth and Dieter Spreen and Julian Webster}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04351.9}, URN = {urn:nbn:de:0030-drops-1175}, doi = {10.4230/DagSemProc.04351.9}, annote = {Keywords: Apartness , constructive , compact uniform space} }
Feedback for Dagstuhl Publishing