OASIcs, Volume 11
CCA 2009, August 18-22, 2009, Ljubljana, Slovenia
Editors: Andrej Bauer, Peter Hertling, and Ker-I Ko
Published in: Dagstuhl Reports, Volume 13, Issue 10 (2024)
Andrej Bauer, Katja Berčič, Florian Rabe, Nicolas Thiéry, and Jure Taslak. Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401). In Dagstuhl Reports, Volume 13, Issue 10, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Article{bauer_et_al:DagRep.13.10.1, author = {Bauer, Andrej and Ber\v{c}i\v{c}, Katja and Rabe, Florian and Thi\'{e}ry, Nicolas and Taslak, Jure}, title = {{Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)}}, pages = {1--23}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2024}, volume = {13}, number = {10}, editor = {Bauer, Andrej and Ber\v{c}i\v{c}, Katja and Rabe, Florian and Thi\'{e}ry, Nicolas and Taslak, Jure}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.1}, URN = {urn:nbn:de:0030-drops-198319}, doi = {10.4230/DagRep.13.10.1}, annote = {Keywords: mathematical knowledge management, mathematical software, formalized mathematics, computer algebra, databases of mathematical structures} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Fabian Immler, Jonas Rädle, and Makarius Wenzel. Virtualization of HOL4 in Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{immler_et_al:LIPIcs.ITP.2019.21, author = {Immler, Fabian and R\"{a}dle, Jonas and Wenzel, Makarius}, title = {{Virtualization of HOL4 in Isabelle}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {21:1--21:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.21}, URN = {urn:nbn:de:0030-drops-110760}, doi = {10.4230/LIPIcs.ITP.2019.21}, annote = {Keywords: Virtualization, HOL4, Isabelle, Isabelle/HOL, Isabelle/ML} }
Published in: Dagstuhl Reports, Volume 8, Issue 8 (2019)
Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi. Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). In Dagstuhl Reports, Volume 8, Issue 8, pp. 130-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@Article{bauer_et_al:DagRep.8.8.130, author = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, title = {{Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)}}, pages = {130--145}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2019}, volume = {8}, number = {8}, editor = {Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.8.8.130}, URN = {urn:nbn:de:0030-drops-102370}, doi = {10.4230/DagRep.8.8.130}, annote = {Keywords: formal methods, formalized mathematics, proof assistant, type theory} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda Proof Assistant. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{bauer_et_al:LIPIcs.TYPES.2016.5, author = {Bauer, Andrej and Gilbert, Ga\"{e}tan and Haselwarter, Philipp G. and Pretnar, Matija and Stone, Christopher A.}, title = {{Design and Implementation of the Andromeda Proof Assistant}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {5:1--5:31}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5}, URN = {urn:nbn:de:0030-drops-98574}, doi = {10.4230/LIPIcs.TYPES.2016.5}, annote = {Keywords: type theory, proof assistant, equality reflection, computational effects} }
Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)
Andrej Bauer, Martin Hofmann, Matija Pretnar, and Jeremy Yallop. From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112). In Dagstuhl Reports, Volume 6, Issue 3, pp. 44-58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@Article{bauer_et_al:DagRep.6.3.44, author = {Bauer, Andrej and Hofmann, Martin and Pretnar, Matija and Yallop, Jeremy}, title = {{From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112)}}, pages = {44--58}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2016}, volume = {6}, number = {3}, editor = {Bauer, Andrej and Hofmann, Martin and Pretnar, Matija and Yallop, Jeremy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.3.44}, URN = {urn:nbn:de:0030-drops-61489}, doi = {10.4230/DagRep.6.3.44}, annote = {Keywords: algebraic effects, computational effects, handlers, implementation techniques, programming languages} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
@Proceedings{bauer_et_al:OASIcs.CCA.2009, title = {{OASIcs, Volume 11, CCA'09, Complete Volume}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2012}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009}, URN = {urn:nbn:de:0030-drops-35738}, doi = {10.4230/OASIcs.CCA.2009}, annote = {Keywords: Mathematics of Computing, Analysis of Algorithms and Problem Complexity} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. i-ii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{bauer_et_al:OASIcs.CCA.2009.2248, author = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, title = {{CCA 2009 Front Matter - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {i--ii}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2248}, URN = {urn:nbn:de:0030-drops-22486}, doi = {10.4230/OASIcs.CCA.2009.2248}, annote = {Keywords: Computable analysis, computability, complexity, Turing machine, constructive mathematics, real number computation, computer arithmetic, exact real ari} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Andrej Bauer, Peter Hertling, and Ker-I Ko. CCA 2009 Preface - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{bauer_et_al:OASIcs.CCA.2009.2249, author = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, title = {{CCA 2009 Preface - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {1--1}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2249}, URN = {urn:nbn:de:0030-drops-22492}, doi = {10.4230/OASIcs.CCA.2009.2249}, annote = {Keywords: Computable analysis, computability, complexity, Turing machine, constructive mathematics, real number computation, computer arithmetic, exact real ari} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Mark Braverman. Computability and Complexity of Julia Sets (Invited Talk). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{braverman:OASIcs.CCA.2009.2250, author = {Braverman, Mark}, title = {{Computability and Complexity of Julia Sets}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {3--3}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2250}, URN = {urn:nbn:de:0030-drops-22508}, doi = {10.4230/OASIcs.CCA.2009.2250}, annote = {Keywords: Computability, computable analysis, dynamical systems, complex dynamics, Julia sets Computability, computable analysis, dynamical systems, complex dynamics, Julia sets} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Vladik Kreinovich. From Interval Computations to Constraint-Related Set Computations: Towards Faster Estimation of Statistics and ODEs under Interval and p-Box Uncertainty (Invited Talk). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 5-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{kreinovich:OASIcs.CCA.2009.2251, author = {Kreinovich, Vladik}, title = {{From Interval Computations to Constraint-Related Set Computations: Towards Faster Estimation of Statistics and ODEs under Interval and p-Box Uncertainty}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {5--16}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2251}, URN = {urn:nbn:de:0030-drops-22516}, doi = {10.4230/OASIcs.CCA.2009.2251}, annote = {Keywords: Interval computations, set computations, probability boxes, uncertainty, efficient algorithms} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Dana Scott. Semilattices, Domains, and Computability (Invited Talk). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{scott:OASIcs.CCA.2009.2252, author = {Scott, Dana}, title = {{Semilattices, Domains, and Computability}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {17--17}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2252}, URN = {urn:nbn:de:0030-drops-22525}, doi = {10.4230/OASIcs.CCA.2009.2252}, annote = {Keywords: Semilattices, domains, computability} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Ning Zhong. Computable Analysis of Differential Equations (Invited Talk). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{zhong:OASIcs.CCA.2009.2253, author = {Zhong, Ning}, title = {{Computable Analysis of Differential Equations}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {19--19}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2253}, URN = {urn:nbn:de:0030-drops-22535}, doi = {10.4230/OASIcs.CCA.2009.2253}, annote = {Keywords: Computable analysis, differential equations} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Martin Escardó. Theory and Practice of Higher-type Computation (Tutorial). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{escardo:OASIcs.CCA.2009.2254, author = {Escard\'{o}, Martin}, title = {{Theory and Practice of Higher-type Computation}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {21--21}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2254}, URN = {urn:nbn:de:0030-drops-22540}, doi = {10.4230/OASIcs.CCA.2009.2254}, annote = {Keywords: Higher-type computation, domain theory, Kleene-Kreisel spaces, Ershov-Scott domains, QCB spaces, equilogical spaces, PCF} }
Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)
Bas Spitters and Russell O'Connor. Computer Verified Exact Analysis (Tutorial). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
@InProceedings{spitters_et_al:OASIcs.CCA.2009.2255, author = {Spitters, Bas and O'Connor, Russell}, title = {{Computer Verified Exact Analysis}}, booktitle = {6th International Conference on Computability and Complexity in Analysis (CCA'09)}, pages = {23--23}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-12-5}, ISSN = {2190-6807}, year = {2009}, volume = {11}, editor = {Bauer, Andrej and Hertling, Peter and Ko, Ker-I}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2255}, URN = {urn:nbn:de:0030-drops-22554}, doi = {10.4230/OASIcs.CCA.2009.2255}, annote = {Keywords: Proof assistant, dependent type theory, constructive analysis} }
Feedback for Dagstuhl Publishing