Horațiu Cheval

Horațiu Cheval

PhD Student,
Research Center for Logic, Optimization and Security,
Department of Computer Science,
Faculty of Mathematics and Computer Science,
University of Bucharest

Associated Researcher,
Institute for Logic and Data Science

I completed my undergraduate studies in Computer Science at the Faculty of Mathematics and Computer Science at the University of Bucharest, with a thesis in the field of proof mining. I then followed the Master's program in Security and Applied Logic at the same institutions. In my Master's thesis I continued the research I started as an undergraduate in proof mining, while also writing my first paper in the field of convex optimization. During the same time, I became interested in type theory and proof assistants, the language I know best being Lean. In September 2021 I became a PhD student in Mathematics supervised by Laurențiu Leuștean. I am also an associated researcher at the Institute for Logic and Data Science.

Publications

Journal papers

• Rates of asymptotic regularity of the Tikhonov-Mann iteration for families of mappings, Accepted for publication in Revue Roumaine de Mathématiques Pures et Appliquées (2024).
• Formal Definitions and Proofs for Partial (Co)Recursive Functions (with David Nowak and Vlad Rusu), Journal of Logical and Algebraic Methods in Programming (2024)
• Linear rates of asymptotic regularity for Halpern-type iterations (with Laurențiu Leuștean), Mathematics of Computation (2024)
• On modified Halpern and Tikhonov-Mann iterations (with Ulrich Kohlenbach and Laurențiu Leuștean), Journal of Optimization Theory and Applications (2023)
• Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration (with Laurențiu Leuștean), Optimization Methods and Software (2022)

Preprints

• Quantitative metastability of the Tikhonov-Mann iteration for countable families of mappings, arXiv:2406.03429 [math.OC] (2024)

Software

• Lean formalization of Applicative Matching Logic (with Bogdan Macovei)
• Lean HOAS implementation of the Dialectica interpretation and logical metatheorems based on it
• Lean formalization of results in H. Cheval and L. Leuștean. Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration, Optimization Methods and Software, 2022.
• Python implementation of various fixed point iteration in W-hyperbolic spaces

Github

CV

CV in pdf format

Talks

Invited talks

• MFO Workshop, Mathematical Logic: Proof Theory, Constructive Mathematics, Oberwolfach, November 12 - 17, 2023
• Logic Colloquium 2023, Special Session on Applied Proof Theory, Milan, June 5-9, 2023

Contributed conference talks

• Logic Colloquium 2024, Göteborg, June 24-28, 2024
• Working Formal Methods Symposium (FROM) 2023, Bucharest, September 21 - 22, 2023
• The Tenth Congress of Romanian Mathematicians, Pitești, June 30 - July 5, 2023
• Workshop for Young Researchers in Mathematics, Bucharest, May 19-20, 2022
• Working Formal Methods Symposium, Timișoara, December 8-9, 2021
• Logic Colloquium 2021, Poznań, July 19-24
• Computability in Europe 2021, Ghent, July 5-9, 2021
• The 22nd annual Graduate Student Conference in Logic, Urbana-Champaign, March 20-21, 2021

Other talks

• EuroProofNet Tutorial on Usable Formal Methods for Security of Systems, Dresden, March 27-28, 2024
• EuroProofNet WG3 Meeting, Timișoara, February 8-9, 2023
• RV/ILDS/LOS InFormal Workshop on Logics, Bucharest, January 26, 2023