Proof assistants are tools that enable the mechanization (proofs checked by a machine) of mathematical theories. Mechanized proofs provide a very high degree of assurance of correctness. This level of assurance is especially necessary for the complex mathematical theory underlying programming languages and program verification. Our research in PLS focuses both on developing the theory underlying these proof assistants (Categorical Type Theory) as well as novel ways of using proof assistants for formalizing mathematical theories, including studying correctness properties of programs and programming languages (Program Verification - Iris). They are also crucial in cybersecurity. 

Since proof assistants and their design are vital for the program logics section, I think the broader social impact flows from that topic.