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

• 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

• Rates of asymptotic regularity of the Tikhonov-Mann iteration for families of mappings, arXiv:2304.11366 [math.OC] (2023)
• Linear rates of asymptotic regularity for Halpern-type iterations (with Laurențiu Leuștean), arXiv:2303.05406 [math.OC] (2023)

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

• Logic Colloquium 2023, Special Session on Applied Proof Theory, Milan, June 5-9, 2023

Contributed conference talks

• 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 WG3 Meeting, Timișoara, February 8-9, 2023
• RV/ILDS/LOS InFormal Workshop on Logics, Bucharest, January 26, 2023