Two papers coauthored by IRIF members will be presented at POPL’20, the main conference on programming languages and programming systems. The papers' topics are reflecting Coq in Coq and how to differentiate higher-order programs.