Research on "Formal Methods in Computing"

On-line tools demonstrations

• Useless-code elimination for a small functional language

• Rank two intersection types for:
  • Local definitions and conditional expressions
  • Modules with symmetric linking (built on top of a small functional language)
  • Polymorphic recursion

• Type Inference for M³ Mobile Ambients

• Type Inference for BoCa

• Isomorphism Checker for Intersection Types