|
|||||
|
These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now. Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions [...] Two versions of this talk were given at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008. Joint work with Paul Taylor. Abstract: Cauchy’s construction of reals as sequences of rational approximations is the theoretical basis for a number of implementations of exact real numbers, while Dedekind’s construction of reals as cuts has [...] With Iztok Kavkler. Abstract: The interval domain was proposed by Dana Scott as a domain-theoretic model for real numbers. It is a successful theoretical idea which also inspired a number of computational models for real numbers. However, current state-of-the-art implementations of real numbers, e.g., Mueller’s iRRAM and Lambov’s RealLib, do not seem to be based on [...] A tutorial presented at the Mathematical Foundations of Programming Semantics XXIII Tutorial Day. With Davorin Lešnik. Abstract: We investigate the relationship between constructive theory of metric spaces and synthetic topology. Connections between these are established by requiring a relationship to exist between the intrinsic and the metric topology of a space. We propose a non-classical axiom which has several desirable consequences, e.g., that all maps between separable metric spaces [...] With Iztok Kavkler. Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program specifications using the realizability interpretation of logic. This helps programmers correctly implement data structures for computable mathematics. RZ does not prescribe a particular method of implementation, but allows programmers to write efficient code by hand, or to extract trusted code [...] With Chris Stone. Abstract: With Alex Simpson. Abstract: We present a constructive meta-theorem about sequential continuity which allows us to conclude from a constructive proof of existence of a function between complete metric spaces satisfying a given system of (functional) equations that there also exists a sequentially continuous function satisfying the system. Presented at: Trends in Constructive mathematics, Frauenwörth am Chimsee, [...] With Chris Stone. Presented at: Reliable Implementation of Real Number Algorithms: Theory and Practice, Dagstuhl Seminar 06021. Abstract: see “Specifications via Realizability (CLASE)”. Talk notes: rz-dagstuhl.pdf (handwritten notes of the talk with examples of how RZ works) At the EST training workshop in Fischbachau, Germany, I gave two lectures on syntehtic computability theory. This version of the talk contains material on recursive analysis which is not found in the MFPS XXI version of a similar talk. Abstract: |
|||||
|
|
|||||
