36 Search Results for "Bauer, Andrej"


Volume

OASIcs, Volume 11

6th International Conference on Computability and Complexity in Analysis (CCA'09)

CCA 2009, August 18-22, 2009, Ljubljana, Slovenia

Editors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Document
Virtualization of HOL4 in Isabelle

Authors: Fabian Immler, Jonas Rädle, and Makarius Wenzel

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We present a novel approach to combine the HOL4 and Isabelle theorem provers: both are implemented in SML and based on distinctive variants of HOL. The design of HOL4 allows to replace its inference kernel modules, and the system infrastructure of Isabelle allows to embed other applications of SML. That is the starting point to provide a virtual instance of HOL4 in the same run-time environment as Isabelle. Moreover, with an implementation of a virtual HOL4 kernel that operates on Isabelle/HOL terms and theorems, we can load substantial HOL4 libraries to make them Isabelle theories, but still disconnected from existing Isabelle content. Finally, we introduce a methodology based on the transfer package of Isabelle to connect the imported HOL4 material to that of Isabelle/HOL.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)

Authors: Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi

Published in: Dagstuhl Reports, Volume 8, Issue 8 (2019)


Abstract
Formalized mathematics is mathematical knowledge (definitions, theorems, and proofs) represented in digital form suitable for computer processing. The central goal of this seminar was to identify the theoretical advances and practical improvements needed in the area of formalized mathematics, in order to make it a mature technology, truly useful to a larger community of students and researchers in mathematics. During the seminar, various software systems for formalization were compared, and potential improvements to existing systems were investigated. There have also been discussions on the representation of algebraic structures in formalization systems.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Design and Implementation of the Andromeda Proof Assistant

Authors: Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)


Abstract
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization). The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped lambda-calculus, and by implementing a simple automated system for managing a universe of types.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112)

Authors: Andrej Bauer, Martin Hofmann, Matija Pretnar, and Jeremy Yallop

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)


Abstract
Dagstuhl Seminar 16112 was devoted to research in algebraic effects and handlers, a chapter in the principles of programming languages which addresses computational effects (such as I/O, state, exceptions, nondeterminism, and many others). The speakers and the working groups covered a range of topics, including comparisons between various control mechanisms (handlers vs. delimited control), implementation of an effect system for OCaml, compilation techniques for algebraic effects and handlers, and implementations of effects in Haskell.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Complete Volume
OASIcs, Volume 11, CCA'09, Complete Volume

Authors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
OASIcs, Volume 11, CCA'09, Complete Volume

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Front Matter
CCA 2009 Front Matter - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis

Authors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
The Sixth International Conference on Computability and Complexity in Analysis, CCA 2009, took place on August 18 to 22, 2009, in Ljubljana, Slovenia. The conference is concerned with Computable Analysis, the theory of computability and complexity over real-valued data. The conference program consisted of 4 invited talks, 2 tutorials of three talks each, and 24 contributed talks. These proceedings contain the abstracts or extended abstracts of the invited talks, tutorials, and a selection of 22 contributed articles.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
CCA 2009 Preface - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis

Authors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
The Sixth International Conference on Computability and Complexity in Analysis, CCA 2009, took place on August 18 to 22, 2009, in Ljubljana, Slovenia. The conference is concerned with Computable Analysis, the theory of computability and complexity over real-valued data. The conference program consisted of 4 invited talks, 2 tutorials of three talks each, and 24 contributed talks. These proceedings contain the abstracts or extended abstracts of the invited talks, tutorials, and a selection of 22 contributed articles.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Invited Talk
Computability and Complexity of Julia Sets (Invited Talk)

Authors: Mark Braverman

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
Studying dynamical systems is key to understanding a wide range of phenomena ranging from planetary movement to climate patterns to market dynamics. Various numerical tools have been developed to address specific questions about dynamical systems, such as predicting the weather or planning the trajectory of a satellite. However, the theory of computation behind these problems appears to be very difficult to develop. In fact, little is known about computability of even the most natural problems arising from dynamical systems. In this talk I will survey the recent study of the computational properties of dynamical systems that arise from iterating quadratic polynomials on the complex plane. These give rise to the amazing variety of fractals known as Julia sets, and are closely connected to the Mandelbrot set. Julia sets are perhaps the most drawn objects in Mathematics due to their fascinating fractal structure. The theory behind them is even more fascinating, and the dynamical systems generating them are in many ways archetypal. I will present both positive and negative results on the computability and complexity of Julia sets. In conclusion of the talk I will discuss possible future directions and challenges in the study of the computability and complexity of dynamical systems.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Invited Talk
From Interval Computations to Constraint-Related Set Computations: Towards Faster Estimation of Statistics and ODEs under Interval and p-Box Uncertainty (Invited Talk)

Authors: Vladik Kreinovich

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
Interval computations estimate the uncertainty of the result of data processing in situations in which we only know the upper bounds $\Delta$ on the measurement errors. In this case, based on the measurement result $\widetilde x$, we can only conclude that the actual (unknown) value $x$ of the desired quantity is in the interval $[\widetilde x-\Delta,\widetilde x+\Delta]$. In interval computations, at each intermediate stage of the computation, we have intervals of possible values of the corresponding quantities. As a result, we often have bounds with excess width. To remedy this problem, in our previous papers, we proposed an extension of interval technique to {\it set computations}, where on each stage, in addition to intervals of possible values of the quantities, we also keep sets of possible values of pairs (triples, etc.). In this paper, we show that in several practical problems, such as estimating statistics (variance, correlation, etc.) and solutions to ordinary differential equations (ODEs) with given accuracy, this new formalism enables us to find estimates in feasible (polynomial) time.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Invited Talk
Semilattices, Domains, and Computability (Invited Talk)

Authors: Dana Scott

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
As everyone knows, one popular notion of Scott domain is defined as a bounded complete algebraic cpo. These are closely related to algebraic lattices: (i) A Scott domain becomes an algebraic lattice with the adjunction of an (isolated) top element. (ii) Every non-empty Scott-closed subset of an algebraic lattice is a Scott domain. Moreover, the isolated ($=$ compact) elements of an algebraic lattice form a semilattice (under join). This semilattice has a zero element, and, provided the top element is isolated, it also has a unit element. The algebraic lattice itself may be regarded as the ideal completion of the semilattice of isolated elements. This is all well known. What is not so clear that is that there is an easy-to-construct domain of countable semilattices giving isomorphic copies of all countably based domains. This approach seems to have advantages over both ``information systems'' or more abstract lattice formulations, and it makes definitions of solutions to domain equations very elementary to justify. The ``domain of domains'' also has an immediate computable structure.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Invited Talk
Computable Analysis of Differential Equations (Invited Talk)

Authors: Ning Zhong

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
In this talk, we discuss some algorithmic aspects of the local and global existence theory for various ordinary and partial differential equations. We will present a sample of results and give some idea of the motivation and general philosophy underlying these results.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Tutorial
Theory and Practice of Higher-type Computation (Tutorial)

Authors: Martin Escardó

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
In higher-type computation, established by Kleene and Kreisel in the late 1950's (independently), one works with the data types obtained from the discrete natural numbers by closing under finite products and function spaces. For the theory of higher-type programming languages, it is natural to work with a corresponding hierarchy, or type structure, of domains, identified by Ershov and Scott in the late 1960's (again independently). The Kleene-Kreisel and Ershov-Scott hierarchies account for total and partial computation respectively. In this tutorial I'll explain the theory and practice of higher-type computation and programming languages, and develop old and new applications. From a theoretical point of view, I'll present Kleene-Kreisel spaces and Ershov-Scott domains, and relate the two. Moreover, I'll discuss common generalizations, chiefly QCB spaces and equilogical spaces, which admit further useful closure properties, and their relationship to TTE (Schroeder, Simpson. Scott, Bauer, Weihrauch and many others). I'll also present a natural higher-type model of computation/programming language, namely PCF (Platek, Scott, Plotkin). From a practical point of view, I'll introduce a fragment of the language Haskell as a faithful implementation of PCF. Moreover, I'll develop and run several examples (and prove theorems about them), pertaining to (i) exhaustive search of infinite sets in finite time in particular Ulrich Berger's algorithm and generalizations), and (ii) computation with real numbers (in particular Alex Simpson's integration algorithm and generalizations).

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Tutorial
Computer Verified Exact Analysis (Tutorial)

Authors: Bas Spitters and Russell O'Connor

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
This tutorial will illustrate how to use the Coq proof assistant to implement effective and provably correct computation for analysis. Coq provides a dependently typed functional programming language that allows users to specify both programs and formal proofs. We will introduce dependent type theory and show how it can be used to develop both mathematics and programming. We will show how to use dependent type theory to implement constructive analysis. Specifically we will cover how to implement effective real numbers and effective integration. This work will be done using the Coq proof assistant. The tutorial will cover how to use the Coq proof assistant. Attendees are encouraged to download and install Coq 8.2 from {\tt http://coq.inria.fr/download} and also download and make the full system of C-CoRN from {\tt http://c-corn.cs.ru.nl/download.html} beforehand.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Computing Conformal Maps onto Canonical Slit Domains

Authors: Valentin V. Andreev and Timothy H. McNicholl

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)


Abstract
We extend the results of (Andreev, Daniel, McNicholl preprint) by computing conformal maps onto the canonical slit domains in (Nehari 1975). Along the way, we demonstrate the computability of solutions to Neuman problems.

Cite as

Valentin V. Andreev and Timothy H. McNicholl. Computing Conformal Maps onto Canonical Slit Domains. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 25-36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{andreev_et_al:OASIcs.CCA.2009.2256,
  author =	{Andreev, Valentin V. and McNicholl, Timothy H.},
  title =	{{Computing Conformal Maps onto Canonical Slit Domains}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{25--36},
  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.2256},
  URN =		{urn:nbn:de:0030-drops-22561},
  doi =		{10.4230/OASIcs.CCA.2009.2256},
  annote =	{Keywords: Computable analysis, conformal mapping}
}
  • Refine by Author
  • 7 Bauer, Andrej
  • 3 Hertling, Peter
  • 3 Ko, Ker-I
  • 2 Brattka, Vasco
  • 2 Gherardi, Guido
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Interoperability
  • 1 Theory of computation → Higher order logic

  • Refine by Keyword
  • 8 Computable analysis
  • 4 constructive analysis
  • 3 complexity
  • 3 computability
  • 3 computable analysis
  • Show More...

  • Refine by Type
  • 35 document
  • 1 volume

  • Refine by Publication Year
  • 31 2009
  • 2 2019
  • 1 2012
  • 1 2016
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail