 In addition to the traditional, foundational branch of proof theory, today there is a good deal of interest in structural proof theory, a branch of the subject that focuses on logical deductive calculi and their properties. This research is closely linked with issues relevant to computer science, having to do with automated deduction, functional programming, and computer aided verification. Here, too, Gentzen-style methods tend to dominate (see again the  entry on proof theory).  But the epsilon calculus can also provide valuable insights; cf. for example Aguilera &amp; Baaz 2019, or the discussion of Herbrand’s theorem above.