Díaz-Caro, Alejandro; Dowek, Gilles Extensional proofs in a propositional logic modulo isomorphisms. (English) Zbl 07751512 Theor. Comput. Sci. 977, Article ID 114172, 17 p. (2023). MSC: 68Qxx PDFBibTeX XMLCite \textit{A. Díaz-Caro} and \textit{G. Dowek}, Theor. Comput. Sci. 977, Article ID 114172, 17 p. (2023; Zbl 07751512) Full Text: DOI arXiv
Díaz-Caro, Alejandro; Dowek, Gilles A new connective in natural deduction, and its application to quantum computing. (English) Zbl 07679990 Theor. Comput. Sci. 957, Article ID 113840, 27 p. (2023). MSC: 81P68 32E05 68N18 03B38 68V15 81P15 81P10 68Q12 PDFBibTeX XMLCite \textit{A. Díaz-Caro} and \textit{G. Dowek}, Theor. Comput. Sci. 957, Article ID 113840, 27 p. (2023; Zbl 07679990) Full Text: DOI
Dowek, Gilles Models and termination of proof reduction in the \(\lambda\Pi\)-calculus modulo theory. (English) Zbl 1442.03009 Chatzigiannakis, Ioannis (ed.) et al., 44th international colloquium on automata, languages, and programming, ICALP 2017, Warsaw, Poland July 10–14, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 80, Article 109, 14 p. (2017). MSC: 03B40 PDFBibTeX XMLCite \textit{G. Dowek}, LIPIcs -- Leibniz Int. Proc. Inform. 80, Article 109, 14 p. (2017; Zbl 1442.03009) Full Text: DOI arXiv
Englander, Cecilia; Dowek, Gilles; Haeusler, Edward Hermann Yet another bijection between sequent calculus and natural deduction. (English) Zbl 1343.03042 Ayala-Rincón, Mauricio (ed.) et al., Proceedings of the 9th workshop on logical and semantic frameworks, with applications (LSFA 2014), Brasilia, Brazil, September 8–9, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 312, 107-124, electronic only (2015). MSC: 03F03 03B20 PDFBibTeX XMLCite \textit{C. Englander} et al., Electron. Notes Theor. Comput. Sci. 312, 107--124 (2015; Zbl 1343.03042) Full Text: DOI
Dowek, Gilles 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). MSC: 01-02 03-03 03B35 03B40 03B70 03Dxx 03Fxx 68-XX 68-02 68-03 68N18 68Qxx 68T15 PDFBibTeX XMLCite \textit{G. Dowek}, Computation, proof, machine. Mathematics enters a new age. Translated from the French by Pierre Guillot and Marion Roman. Cambridge: Cambridge University Press (2015; Zbl 1318.01002)
Dowek, Gilles A theory independent Curry-De Bruijn-Howard correspondence. (English) Zbl 1367.03029 Czumaj, Artur (ed.) et al., Automata, languages, and programming. 39th international colloquium, ICALP 2012, Coventry, UK, July 9–13, 2012. Proceedings, Part II. Berlin: Springer (ISBN 978-3-642-31584-8/pbk). Lecture Notes in Computer Science 7392, 13-15 (2012). MSC: 03B40 03B35 03F03 PDFBibTeX XMLCite \textit{G. Dowek}, Lect. Notes Comput. Sci. 7392, 13--15 (2012; Zbl 1367.03029) Full Text: DOI
Dowek, Gilles 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). MSC: 01-02 03-03 03B35 03B40 03B70 03Dxx 03Fxx 68-02 68-03 68N18 68Qxx 68T15 PDFBibTeX XMLCite \textit{G. Dowek}, Les métamorphoses du calcul. Une étonnante histoire de mathématiques. Reprint of the 2007 edition. Paris: Éditions Le Pommier (2011; Zbl 1360.01012)
Dowek, Gilles Proofs and algorithms. An introduction to logic and computability. (English) Zbl 1230.03001 Undergraduate Topics in Computer Science. New York, NY: Springer (ISBN 978-0-85729-120-2/pbk; 978-0-85729-121-9/ebook). xii, 155 p. (2011). Reviewer: Damas Gruska (Bratislava) MSC: 03-01 68-01 03B10 03B25 03B35 03B40 03B70 03C07 03D10 03D20 03D35 03F03 68Q05 68W01 PDFBibTeX XMLCite \textit{G. Dowek}, Proofs and algorithms. An introduction to logic and computability. New York, NY: Springer (2011; Zbl 1230.03001) Full Text: DOI
Dowek, Gilles Proofs and algorithms. An introduction to logic and computability. (Les démonstrations et les algorithmes. Introduction à la logique et à la calculabilité.) (French) Zbl 1230.03002 Palaiseau: Les Éditions de l’École Polytechnique (ISBN 978-2-7302-1569-5). 195 p. (2010). MSC: 03-01 68-01 03B10 03B25 03B35 03B40 03B70 03C07 03D10 03D20 03D35 03F03 68Q05 68W01 PDFBibTeX XMLCite \textit{G. Dowek}, Les démonstrations et les algorithmes. Introduction à la logique et à la calculabilité. Palaiseau: Les Éditions de l'École Polytechnique (2010; Zbl 1230.03002)
Dowek, Gilles On the convergence of reduction-based and model-based methods in proof theory. (English) Zbl 1183.03061 Log. J. IGPL 17, No. 5, 489-497 (2009). Reviewer: M. Yasuhara (Princeton) MSC: 03F05 03C30 03F03 03B35 PDFBibTeX XMLCite \textit{G. Dowek}, Log. J. IGPL 17, No. 5, 489--497 (2009; Zbl 1183.03061) Full Text: DOI
Dowek, Gilles 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). Reviewer: Radoslav M. Dimitrić (Uniontown) MSC: 01-02 03-03 03B35 03B40 03B70 03Dxx 03Fxx 68-02 68-03 68N18 68Qxx 68T15 PDFBibTeX XMLCite \textit{G. Dowek}, Les métamorphoses du calcul. Une étonnante histoire de mathématiques. Paris: Éditions Le Pommier (2007; Zbl 1161.01001)
Dowek, Gilles Introduction to proof theory. (English) Zbl 1134.03031 Schwichtenberg, Helmut (ed.) et al., Proof technology and computation. Papers from the summer school, Marktoberdorf, Germany, July 29–August 10, 2003. Amsterdam: IOS Press (ISBN 1-58603-625-4/hbk). NATO Science Series III: Computer & Systems Sciences 200, 57-126 (2006). Reviewer: M. Yasuhara (Princeton) MSC: 03F03 03F05 03-02 PDFBibTeX XMLCite \textit{G. Dowek}, NATO Sci. Ser. III, Comput. Syst. Sci. 200, 57--126 (2006; Zbl 1134.03031)
Dowek, Gilles Type theory and proof processing systems. (La th’eorie des types et les systémes informatiques de traitement de démonstrations mathematiques.) (French. English summary) Zbl 1127.03319 Math. Sci. Hum., Math. Soc. Sci. 165, 13-29 (2003). MSC: 03B15 03B35 68T15 PDFBibTeX XMLCite \textit{G. Dowek}, Math. Sci. Hum., Math. Soc. Sci. 165, 13--29 (2003; Zbl 1127.03319)
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic. (English) Zbl 0972.03012 Math. Struct. Comput. Sci. 11, No. 1, 21-45 (2001). MSC: 03B35 03B15 68T15 PDFBibTeX XMLCite \textit{G. Dowek} et al., Math. Struct. Comput. Sci. 11, No. 1, 21--45 (2001; Zbl 0972.03012) Full Text: DOI
Dowek, Gilles; Werner, Benjamin Proof normalization modulo. (English) Zbl 0944.03052 Altenkirch, Thorsten (ed.) et al., Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27-31, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1657, 62-77 (1999). MSC: 03F05 03B35 03B15 03B10 PDFBibTeX XMLCite \textit{G. Dowek} and \textit{B. Werner}, Lect. Notes Comput. Sci. 1657, 62--77 (1999; Zbl 0944.03052)
Dowek, Gilles Proof normalization for a first-order formulation of higher-order logic. (English) Zbl 0905.03036 Gunter, Elsa L. (ed.) et al., Theorem proving in higher order logics. 10th international conference, TPHOLs ’97. Murray Hill, NJ, USA. August 19–22, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1275, 105-119 (1997). MSC: 03F05 03B15 PDFBibTeX XMLCite \textit{G. Dowek}, Lect. Notes Comput. Sci. 1275, 105--119 (1997; Zbl 0905.03036)
Dowek, Gilles A complete proof synthesis method for the cube of type systems. (English) Zbl 0789.68123 J. Log. Comput. 3, No. 3, 287-315 (1993). Reviewer: Dowek, Gilles MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{G. Dowek}, J. Log. Comput. 3, No. 3, 287--315 (1993; Zbl 0789.68123) Full Text: DOI