Sequential two-level formalization of mathematical theoriesдоклад на конференции