Мадс Тофте (родился 20 апреля 1959 года) — датский учёный-компьютерщик , внёсший особый вклад в функциональное программирование и стандартный язык программирования ML .
Тофте родился в Lyngby , Дания и вырос в Holbæk , Дания . Он изучал информатику и математику в Университете Копенгагена , где получил степень магистра (под руководством Нила Д. Джонса ) в 1984 году; затем в Университете Эдинбурга , где получил степень доктора философии в 1988 году (под руководством Робина Милнера ). Он является почетным доктором 2007 года Университета Кингстона .
В своей магистерской диссертации 1984 года [1] и предыдущей работе он исследовал и формализовал генератор компилятора CERES (совместно с Нилом Д. Джонсом) и показал, что (1) генератор компилятора сам по себе является компилятором из определений языка в компиляторы; и (2) при соответствующих предположениях существует определение языка, которое, будучи применено к себе, генерирует генератор компилятора. Это тесно связано с самоприменением в частичной оценке .
В своей докторской диссертации он разработал и доказал правильность первой системы звуковых типов для полиморфных ссылок в стиле ML , важной открытой проблемы того времени. Более того, он формализовал вариант модульной системы языка программирования Standard ML .
Мадс Тофте является соавтором Определения [2] Стандартного ML и соответствующего Комментария, вероятно, наиболее точного описания, разработанного для любого реалистичного языка программирования. Он был соавтором ML Kit, реализации Стандартного ML, структура которой тесно связана с Определением.
Впоследствии он разработал (совместно с Жаном-Пьером Тальпеном) понятие регионального вывода , метод анализа программ и управления памятью , который позволяет избежать или свести к минимуму использование сборки мусора . Эта работа была впервые опубликована [3] в POPL 1994, а в 2005 году она получила премию Ассоциации вычислительной техники (ACM) POPL 1994 Most Influential Paper Award.
В конце девяностых он совместно (совместно с Фрицем Хенглейном и другими) разработал систему типов и сложный инструмент под названием AnnoDomini для смягчения проблемы 2000 года в программном обеспечении COBOL . Инструмент анализирует устаревшие программы, чтобы обнаружить все поля данных, которые используются как даты. Эта работа была представлена в приглашенном докладе POPL 1999. [4]
В апреле 1999 года он был назначен первым управляющим директором Копенгагенского университета информационных технологий . Он курировал создание университета с нуля, найм преподавателей/сотрудников, набор студентов и разработку учебных программ. Первые студенты начали обучение 5 месяцев спустя в сентябре 1999 года. С 2003 года он является вице-канцлером Копенгагенского университета информационных технологий .
В апреле 2018 года было объявлено, что он покинет Копенгагенский ИТ-университет в конце года. В январе 2019 года он объявил, что уедет из Дании, чтобы быть со своей дочерью, из-за иммиграционных законов Дании, которые не позволяли ей въехать в страну. [5]