Found 12 Documents (Results 1–12)
Homotopy type theory as internal languages of diagrams of \(\infty\)-logoses. (English) Zbl 07929320
Gaboardi, Marco (ed.) et al., 8th international conference on formal structures for computation and deduction, FSCD 2023, Rome, Italy, July 3–6, 2023. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 260, Article 5, 19 p. (2023).
Gödel’s theorem without tears – essential incompleteness in synthetic computability. (English) Zbl 07918709
Klin, Bartek (ed.) et al., 31st EACSL annual conference on computer science logic, CSL 2023, February 13–16, 2023, Warsaw, Poland. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 252, Article 30, 18 p. (2023).
MSC:
03B70
Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version. (English) Zbl 07695716
MSC:
68V15
Undecidability of dyadic first-order logic in Coq. (English) Zbl 07881132
Andronick, June (ed.) et al., 13th international conference on interactive theorem proving, ITP 2022, Haifa, Israel, August 7–10, 2022. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 237, Article 19, 19 p. (2022).
MSC:
68V15
Synthetic Kolmogorov complexity in coq. (English) Zbl 07881125
Andronick, June (ed.) et al., 13th international conference on interactive theorem proving, ITP 2022, Haifa, Israel, August 7–10, 2022. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 237, Article 12, 19 p. (2022).
MSC:
68V15
An analysis of Tennenbaum’s theorem in constructive type theory. (English) Zbl 1541.03167
Felty, Amy P. (ed.), 7th international conference on formal structures for computation and deduction, FSCD 2022, Haifa, Israel, August 2–5, 2022. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 228, Article 9, 19 p. (2022).
Sheaf semantics of termination-insensitive noninterference. (English) Zbl 07853711
Felty, Amy P. (ed.), 7th international conference on formal structures for computation and deduction, FSCD 2022, Haifa, Israel, August 2–5, 2022. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 228, Article 5, 19 p. (2022).
MSC:
68Qxx
Synthetic undecidability and incompleteness of first-order axiom systems in Ccoq. (English) Zbl 07699440
Cohen, Liron (ed.) et al., 12th international conference on interactive theorem proving, ITP 2021, Rome, Italy, virtual conference, June 29 – July 1, 2021. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 193, Article 23, 20 p. (2021).
MSC:
68V15
Realizability. An introduction to its categorical side. (English) Zbl 1225.03002
Studies in Logic and the Foundations of Mathematics 152. Amsterdam: Elsevier (ISBN 978-0-444-51584-1/hbk). xvi, 310 p. (2008).
Reviewer: Colin McLarty (MR2479466)
Filter Results by …
Document Type
- Journal Articles (4)
- Collection Articles (7)
- Books (1)
all
top 5
Author
- Kirst, Dominik (6)
- Hermes, Marc (4)
- van Oosten, Jaap (2)
- Bauer, Andrej (1)
- Dudenhefner, Andrej (1)
- Forster, Yannick (1)
- Harper, Robert (1)
- Hostert, Johannes (1)
- Kunze, Fabian (1)
- Lauermann, Nils (1)
- Peters, Benjamin (1)
- Simpson, Alex K. (1)
- Sterling, Jonathan (1)
- Uemura, Taichi (1)
