Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017

DOI10.4171/OWR/2017/53zbMATH Open1409.00077OpenAlexW4230543667WikidataQ128724227 ScholiaQ128724227MaRDI QIDQ1731963FDOQ1731963

Authors:

Publication date: 15 March 2019

Published in: Oberwolfach Reports (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.4171/owr/2017/53

Recommendations

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Mathematical logic: Proof theory, constructive mathematics. Abstracts from the workshop held April 6--12, 2008.
• Proceedings of the fifth international workshop on classical logic and computation, CL\&C 2014, Vienna, Austria, July 13, 2014
• Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
• Mathematical logic: proof theory, type theory and constructive mathematics

Mathematics Subject Classification ID

Proceedings of conferences of miscellaneous specific interest (00B25) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Proof theory and constructive mathematics (03Fxx) Collections of abstracts of lectures (00B05)

Cites Work

• Title not available (Why is that?)
• Non-constructivity in Kan simplicial sets
• Convex analysis and monotone operator theory in Hilbert spaces
• Structural proof theory. With an appendix by Aarne Ranta
• Cut Elimination in the Presence of Axioms
• A globalization of the Hahn-Banach theorem
• Real number computation through Gray code embedding.
• An abstract data type for real numbers
• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• Title not available (Why is that?)
• Subsystems of second order arithmetic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proving open properties by induction
• A course in constructive algebra
• A universal Krull-Lindenbaum theorem
• Title not available (Why is that?)
• Weak Sharp Minima in Mathematical Programming
• A logical approach to abstract algebra
• Hidden constructions in abstract algebra. Krull Dimension of distributive lattices and commutative rings
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Results on the propositional \(\mu\)-calculus
• Rapidly growing Ramsey functions
• Title not available (Why is that?)
• Proof analysis in modal logic
• Realizability. An introduction to its categorical side
• Title not available (Why is that?)
• Slow consistency
• Geometrisation of first-order logic
• The strength of infinitary Ramseyan principles can be accessed by their densities
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• An application of proof mining to nonlinear iterations
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Dependent choice, `quote' and the clock
• Existential witness extraction in classical realizability and via a negative translation
• Title not available (Why is that?)
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory
• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the restricted ordinal theorem
• Making the use of maximal ideals constructive
• Sequential games and optimal strategies
• Selection functions, bar recursion and backward induction
• Revisiting Zariski main theorem from a constructive point of view
• Title not available (Why is that?)
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Constructive finite free resolutions
• Accessible Independence Results for Peano Arithmetic
• Goodstein sequences for prominent ordinals up to the Bachmann-Howard ordinal
• Classifying phase transition thresholds for Goodstein sequences and hydra games
• Transfinite ordinals in recursive number theory
• Dynamical method in algebra: Effective Nullstellensätze
• Syntactic cut-elimination for common knowledge
• Realizability algebras. II: New models of \(\mathrm{ZF} + \mathrm{DC}\)
• Realizability algebras: a program to well order \(\mathbb R\)
• Title not available (Why is that?)
• Canonical completeness of infinitary \(\mu \)
• Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
• Rudiments of \(\mu\)-calculus
• Goodstein sequences for prominent ordinals up to the ordinal of \(\Pi^1_1\)-\(\mathrm{CA}_0\)
• Proof lengths for instances of the Paris-Harrington principle
• Title not available (Why is that?)
• Generic cuts in models of arithmetic
• The generalised type-theoretic interpretation of constructive set theory
• Convergence rate analysis for averaged fixed point iterations in common fixed point problems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theories, sites, toposes. Relating and studying mathematical theories through topos-theoretic `bridges'
• Proof theory in the abstract
• Cobham recursive set functions and weak set theories
• Cobham recursive set functions
• Eliminating disjunctions by disjunction elimination
• Lebesgue numbers and Atsuji spaces in subsystems of second-order arithmetic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logic for Gray-code computation
• Computability theory, nonstandard analysis, and their connections
• Syntactic forcing models for coherent logic
• The Frobenius condition, right properness, and uniform fibrations
• Slow reflection
• Proof analysis for Lewis counterfactuals
• Extracting imperative programs from proofs: In-place Quicksort
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• A sequent calculus for preferential conditional logic based on neighbourhood semantics
• Computational problems in metric fixed point theory and their Weihrauch degrees
• Title not available (Why is that?)
• Extension by conservation. Sikorski's theorem
• Non-monotonic pre-fix points and learning
• Some observations on the logical foundations of inductive theorem proving
• Weihrauch Complexity in Computable Analysis
• Ackermannian Goodstein principles for first order Peano arithmetic
• Modalities in homotopy type theory
• Connected choice and the Brouwer fixed point theorem

Cited In (4)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
• Mathematical logic: Proof theory, constructive mathematics. Abstracts from the workshop held April 6--12, 2008.
• Proceedings of the fifth international workshop on classical logic and computation, CL\&C 2014, Vienna, Austria, July 13, 2014

Uses Software

• Coq
• Isabelle
• APS-1
• Nuprl
• Minlog
• Z
• Pesca
• cubicaltt
• Archive Formal Proofs

This page was built for publication: Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1731963)