Modal Logic in Higher-order Logic

since it combines limited higher-order expressivity with
decidability. It comes with an idiosyncratic setup rather
different from classical logic. In this talk I will show
that modal logic can be obtained as a subsystem of higher-order
logic, and that this approach brings considerable simplifications
as it comes to extensions and decision algorithms.

The talk is based on joint work with Moritz Hardt and Mark Kaminski.