My formalization project

Pietro Monticone