×

Found 800 Documents (Results 1–100)

100
MathJax

Logic and verification of product configuration in the automotive industry. (English) Zbl 07543891

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 387-408 (2022).
PDF BibTeX XML Cite
Full Text: DOI

The Braga method: extracting certified algorithms from complex recursive schemes in Coq. (English) Zbl 07543890

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 305-386 (2022).
PDF BibTeX XML Cite
Full Text: DOI

An Ad-Hoc semantics to study structural properties of types. (English) Zbl 07543889

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 267-303 (2022).
PDF BibTeX XML Cite
Full Text: DOI

Formal topology and univalent foundations. (English) Zbl 07543888

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 255-266 (2022).
PDF BibTeX XML Cite
Full Text: DOI

A uniform characterization of \(\Sigma_1\)-reflection over the fragments of Peano arithmetic. (English) Zbl 07543887

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 189-253 (2022).
PDF BibTeX XML Cite
Full Text: DOI

Generalized spaces for constructive algebra. (English) Zbl 07543886

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 99-187 (2022).
PDF BibTeX XML Cite
Full Text: DOI

From intuitionistic mathematics to point-free topology. (English) Zbl 07543885

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 55-98 (2022).
PDF BibTeX XML Cite
Full Text: DOI

Conceptions of proof from aristotle to Gentzen’s calculi. (English) Zbl 07543884

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 33-54 (2022).
PDF BibTeX XML Cite
Full Text: DOI

Proof and computation: perspectives for mathematics, computer science, and philosophy. (English) Zbl 07543883

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 1-32 (2022).
PDF BibTeX XML Cite
Full Text: DOI

Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. (English) Zbl 07380372

Hackensack, NJ: World Scientific (ISBN 978-981-12-3647-1/hbk; 978-981-12-3649-5/ebook). xvi, 408 p. (2022).
PDF BibTeX XML Cite
Full Text: DOI

Well-partial orderings and their maximal order types. (English) Zbl 07218748

Schuster, Peter M. (ed.) et al., Well-quasi orders in computation, logic, language and reasoning. A unifying concept of proof theory, automata theory, formal languages and descriptive set theory. Based on the minisymposium on well-quasi orders: from theory to applications within the Jahrestagung der Deutschen Mathematiker-Vereinigung (DMV), Hamburg, Germany, September 21–25, 2015 and the Dagstuhl seminar 16031 on well quasi-orders in computer science, Schloss Dagstuhl, Germany, January 17–22, 2016. Cham: Springer. Trends Log. Stud. Log. Libr. 53, 351-391 (2020).
MSC:  03Fxx 03Exx 03Dxx
PDF BibTeX XML Cite
Full Text: DOI

Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. (English) Zbl 1431.03011

Synthese Library 412. Cham: Springer (ISBN 978-3-030-20446-4/hbk; 978-3-030-20447-1/ebook). x, 374 p. (2019).
PDF BibTeX XML Cite
Full Text: DOI

Proof and computation. Digitization in mathematics, computer science, and philosophy. Based on the international autumn school “Proof and computation”, Fischbachau, Germany, October 3–8, 2016. (English) Zbl 1400.03005

Hackensack, NJ: World Scientific (ISBN 978-981-3270-93-0/hbk; 978-981-3270-95-4/ebook). viii, 291 p. (2018).
PDF BibTeX XML Cite
Full Text: DOI

The computational content of nonstandard analysis. (English) Zbl 07440186

Kohlenbach, Ulrich (ed.) et al., Proceedings of the sixth international workshop on classical logic and computation, CL&C 2016, Porto, Portugal, June 23, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 213, 24-40 (2016).
PDF BibTeX XML Cite
Full Text: arXiv Link

Intuitionistic provability versus uniform provability in \(\mathsf{RCA}\). (English) Zbl 1461.03009

Beckmann, Arnold (ed.) et al., Evolving computability. 11th conference on computability in Europe, CiE 2015, Bucharest, Romania, June 29 – July 3, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9136, 186-195 (2015).
PDF BibTeX XML Cite
Full Text: DOI

Computation, proof, machine. Mathematics enters a new age. Translated from the French by Pierre Guillot and Marion Roman. (English) Zbl 1318.01002

Cambridge: Cambridge University Press (ISBN 978-0-521-13377-7/pbk; 978-0-521-11801-9/hbk). viii, 152 p. (2015).
PDF BibTeX XML Cite

Proof mining and combinatorics. Program extraction for Ramsey’s theorem for pairs. (English) Zbl 1262.03003

Darmstadt: TU Darmstadt, Fachbereich Mathematik (Diss.). 147 p. (2012).
PDF BibTeX XML Cite
Full Text: Link

The metamorphoses of the calculus. An amazing history of mathematics. Reprint of the 2007 edition. (Les métamorphoses du calcul. Une étonnante histoire de mathématiques.) (French) Zbl 1360.01012

Poche. Paris: Éditions Le Pommier (ISBN 978-2-7465-0561-2/pbk). 224 p. (2011).
PDF BibTeX XML Cite

Towards a formal theory of computability. (English) Zbl 1245.03064

Schindler, Ralf (ed.), Ways of proof theory. Collected papers by speakers of the colloquium and workshop held on the occasion of the retirement of Wolfram Pohlers, July 17–19, 2008, Münster, Germany. Frankfurt am Main: Ontos Verlag (ISBN 978-3-86838-087-3/hbk). Ontos Mathematical Logic 2, 257-282 (2010).
MSC:  03D65 03F65
PDF BibTeX XML Cite

Mathematical logic with special reference to the natural numbers. Paperback reprint of the 1972 edition. (English) Zbl 1156.03002

Cambridge: Cambridge University Press (ISBN 978-0-521-09058-2/pbk). xvi, 638 p. (2008).
PDF BibTeX XML Cite

Recursion on the partial continuous functionals. (English) Zbl 1137.03035

Dimitracopoulos, Costas (ed.) et al., Logic colloquium 2005. Proceedings of the annual European summer meeting of the Association for Symbolic Logic (ASL), Athens, Greece, July 28–August 3, 2005. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Logic (ASL) (ISBN 978-0-521-88425-9/hbk). Lecture Notes in Logic 28, 173-201 (2008).
MSC:  03F65 03D65 03D75
PDF BibTeX XML Cite

The metamorphoses of the calculus. An amazing history of mathematics. (Les métamorphoses du calcul. Une étonnante histoire de mathématiques.) (French) Zbl 1161.01001

Paris: Éditions Le Pommier (ISBN 978-2-7465-0324-3/pbk). 224 p. (2007).
PDF BibTeX XML Cite

First steps in synthetic computability theory. (English) Zbl 1273.03144

Escardó, M. (ed.) et al., Proceedings of the 21st annual conference on mathematical foundations of programming semantics (MFPS XXI), University of Birmingham, Birmingham, UK, May 18–21, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 155, 5-31 (2006).
PDF BibTeX XML Cite
Full Text: Link

\(\Pi_1^0\) classes – structure and applications. (English) Zbl 0962.03040

Cholak, Peter A. (ed.) et al., Computability theory and its applications. Current trends and open problems. Proceedings of a 1999 AMS-IMS-SIAM joint summer research conference, Boulder, CO, USA, June 13-17, 1999. Providence, RI: American Mathematical Society (AMS). Contemp. Math. 257, 39-59 (2000).
PDF BibTeX XML Cite

Computability. Computable functions, logic, and the foundations of mathematics. With “Computability and undecidability—a timeline. The story of the development of computable functions and the undecidability of arithmetic to 1970” by Richard L. Epstein. 2nd ed. (English) Zbl 0951.03001

Belmont, CA: Wadsworth/Thomson Learning. 299 p., 38 p. (2000).
PDF BibTeX XML Cite

The contribution of Polish logicians to recursion theory. (English) Zbl 1018.03005

Kijania-Placek, Katarzyna (ed.) et al., The Lvov-Warsaw school and contemporary philosophy. Papers from the conference, Lviv (Lvov), Ukraine, November 15-17, 1995 and Warsaw, Poland, November 19-21, 1995. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 273, 265-282 (1998).
MSC:  03-03 03Dxx 01A60
PDF BibTeX XML Cite

Filter Results by …

Document Type

Reviewing State

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Classification

Biographic Reference

all top 3

Software