Ulrich Berger

Some slides

• Prototype implementation of a case study on infinite Gray code (written in Haskell, 2020)


• Towards the extraction of clause learning (i.w.w. Andrew Lawrence and Monika Seisenberger) Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2020), Faro (Portugal, online), August 31, 2020


• From Brouwer's Thesis to the Fan Functional University of Birmingham, Theoretical Computer Science Seminar, February 21, 2020


• Algorithmic aspects of least and greatest fixed points Algebra and Algorithms, Djerba (Tunisia), 4-6 February 2020


• Logical relations and feasibility in higher types Higher-order complexity and its applications, Shonan, Japan, 9 October 2019


• On the constructive content of proofs in abstract analysis Proof and translation: Glivenko's theorem 90 years after, CLMPST, Prague, August 9, 2019


• Realizability for abstract mathematics Facets of realizability, ENS Paris-Saclay, 1-3 July 2019


• BCTCS 2020 Swansea


• IFP - A Logic for Program Extraction BCTCS, Durham, April 17, 2019
  ( presentation)


• Extracting the Fan Functional Theory Seminar, RIMS, Kyoto University, January 17, 2019
  ( presentation)


• On the constructive content of proofs in abstract analysis Helsinki Logic Seminar, December 19, 2018
  ( presentation)


• Program extraction from proofs Autumn School ``Proof and Computation'', Fischbachau, September 16-22, 2018
  ( Swansea University Logic Notes)
  (Interactive Prover (written in Haskell))


• On the computational content of Brouwer's Thesis Workshop on Constructive Mathematics, Hausdorff Institute, Bonn, August 6-10, 2018
  
  
• From abstract mathematics to verified programs Hilbert-Bernays Summer School on Logic and Computation, Göttingen, July 23-27, 2018
  ( Swansea University Logic Notes)
  (Interactive Prover (written in Haskell))


• Scott Domains for Denotational Semantics and Program Extraction Workshop DOMAINS, 7-8 July, 2018, Oxford (part of FLoC)


• CS-205 Chapter 6


• Concurrent and nondeterministic program extraction (handout) Workshop on Intersection Types, Paris, 13 June 2016


• Concurrent and nondeterministic program extraction Workshop on Intersection Types, Paris, 13 June 2016


• A coinductive approach to computable analysis Duality in Computer Science, Dagstuhl, 31 July 2013


• Program Extraction in Church's Simple Theory of Types with Applications to Computable Analysis CCA, Nancy, 9 July 2013


• Coinduction and program extraction in computable analysis ( handout) , CLMPS, Nancy, 25 July 2011


• Program extraction in computable analysis , CiE, Sofia, 29 June 2011


• Program extraction from proofs , MFPS, Pittsburgh, 25 May 2011


• Program extraction from proofs: induction and coinduction , Nottingham, 12 February 2010


• A coinductive approach to exact real number computation talk at the workshop New Interactions between Analysis, Topology, and Computation , Birmingham, 7 January 2009


• A coinductive approach to digital computation talk at the workshop Domains IX , University of Sussex, Brighton, 22-24 September, 2008


• From coinductive proofs to exact real arithmetic invited talk at Workshop on Proof Theory , Bern, 9-10 July, 2008


• A domain-theoretic characterisation of strong normalisation in the Lambda-R-calculus, invited talk at Domains VIII , Novosibirsk, 11-15 September, 2007


• A domain-theoretic strong normalisation theorem, invited talk at Methods of Proof Theory in Mathematics , Bonn, 3-10 June, 2007


• Functional concepts in C++, talk at Computability in Europe , Swansea, 30 June - 5 July, 2006


• Semantic normalisation proofs, talk at Types 2006 , Nottingham, 18-21 April, 2006

• Back to my Homepage
• List of publications
• Recent papers and drafts