题目：Higher-order rewriting systems, categorial algebras and Curry-Howard isomorphisms
报告人：Enric Cosme Llópez（江苏省特聘教授）
时间：2025年2月28日9:30-10:30
地点：36-507
报告摘要：This presentation explores the Curry-Howard correspondence, which links mathematical proofs to computer programs. The author discusses formal derivation systems based on rewriting rules, where paths between terms represent simplified proofs, forming a category with algebraic structures. The work extends to second-order rewriting systems, introducing second-order paths and a corresponding second-order Curry-Howard isomorphism. It is based on the preprint J. Climent Vidal and E. Cosme Llópez. From higher-order rewriting systems to higher-order categorial algebras and higher-order Curry-Howard isomorphisms ArXiv https://arxiv.org/abs/2402.12051.
报告人简介：Enric Cosme Llópez holds a degree in Mathematics from the University of Valencia, a Master's in Pure and Applied Logic from the University of Barcelona and the Polytechnic University of Catalonia, and a Ph.D. in Mathematics from the University of Valencia. His doctoral thesis, titled “Some contributions to the algebraic theory of automata”, was supervised by Professors Adolfo Ballester Bolinches and Jean-Éric Pin. Currently, he is an associate professor at the University of Valencia and a Jiangsu specially-appointed professor at Nantong University for the next three years. His research focuses on the algebraic study of automata theory and formal languages, which are fundamental to computer science. He employs universal algebra, many-sorted algebra, and category theory as key tools in his work. In this talk, he will provide an introduction to his recent research on rewriting systems.
