Labs in Kyoto University, Research Institute for Mathematical Sciences, Laboratory for Computational Mechanisms

0 student voices

A lab that studies proofs themselves from both mathematical and computational perspectives.

The Terui Lab studies proofs themselves from the standpoint of mathematical logic. A proof is a means of doing mathematics, but it can also be an object of mathematics: when represented appropriately, the mathematical structure behind it comes into view. Under the Curry–Howard correspondence, a proof can be regarded as (to a certain extent) the same thing as a functional program, so it also has an aspect as a "medium of computation." The lab approaches the subject from various perspectives, including computational complexity, games, denotational semantics, and algebraic semantics.

#Mathematical logic #Proof theory #Lambda calculus