Na próxima quinta-feira, 05, de 15h às 16h, na sala 2015 do Instituto de Ciências Exatas (ICEx), haverá a palestra “From Sets to Types: using the B Method with modern proof tools”, com o doutorando no Inria, LORIA, Nancy, França, Vincent Trélat. Abaixo, em inglês, informações sobre o palestrante e resumo da palestra.
SPEAKER: Vincent Trélat
I am a Ph.D. student at Inria, LORIA, Nancy, France. My main research interests are logic, formal methods, theorem proving, set theory and automated reasoning. During my Ph.D., I have been developing BEer, a tool that encodes B proof obligations in SMT-LIB 2.7 using higher-order logic.
TITLE: From Sets to Types: using the B Method with modern proof tools
Modern computer-assisted proofs sit at the intersection of type-theoretical foundations (as in proof assistants) and set-theoretical foundations (as in standard mathematics), and the choice of theoretical foundations strongly influences automation and expressiveness.
My research studies this gap in practice by tracking how proof obligations from the B method change shape when moved between these worlds.
On the automation side, BEer connects B proof obligations to modern higher-order SMT solvers; while on the interactive side, BARReL acts as a backend for the B method in Lean.
I will present both tools and show practical examples of how they help discharge B proof obligations.
