Тобиас Нипков

Немецкий учёный-компьютерщик (родился в 1958 году)

Тобиас Нипков (родился в 1958 году) — немецкий учёный-компьютерщик.

Карьера

Нипков получил диплом магистра наук в области компьютерных наук на факультете компьютерных наук Высшей технической школы Дармштадта в 1982 году и степень доктора философии в Манчестерском университете в 1987 году.

С 1987 года он работал в Массачусетском технологическом институте , в 1989 году перешел в Кембриджский университет , а в 1992 году — в Мюнхенский технический университет , где был назначен профессором теории программирования .

С 2011 года он является председателем группы логики и верификации.

Он известен своей работой в области интерактивного и автоматического доказательства теорем , в частности, помощником по доказательству Isabelle ; он был редактором журнала Journal of Automated Reasoning до 1 января 2021 года. ^[1] Кроме того, он фокусируется на семантике языков программирования , системах типов и функциональном программировании . ^[2]

В 2021 году он получил премию Эрбрана «в знак признания его лидерства в разработке Isabelle и связанных с ним инструментов, что привело к существенному вкладу в основы, автоматизацию и использование помощников доказательства в широком спектре приложений, а также его успешных усилий по повышению наглядности автоматизированных рассуждений» ^{[3] .}

В 2022 году он был избран членом Academia Europaea . ^[4]

Избранные публикации

• Мартин, У. и Нипков, Т. (1986). «Унификация в булевых кольцах». В Йорге Х. Зикманне (ред.). Труды 8-й конференции по автоматизированной дедукции . LNCS . Т. 230. Springer. С. 506–513.
• Тобиас Нипков (1987). Поведенческие концепции реализации недетерминированных типов данных (диссертация доктора философии). Отчет кафедры компьютерных наук. Том UMCS-87-5-3. Манчестерский университет.
• Нипков, Т. (1989). «Объединение алгоритмов сопоставления: прямоугольный случай». В Нахум Дершовиц (ред.). Методы переписывания и приложения, 3-я международная конференция, RTA-89 . LNCS. Том 355. Springer. стр. 343–358.
• Тобиас Нипков (1990). «Унификация в первичных алгебрах, их степенях и их многообразиях». Журнал ACM . 37 (4): 742–776. doi : 10.1145/96559.96569 . S2CID  14940917.
• Нипков, Т. и Цянь, З. (1991). «Модулярное E-объединение высшего порядка». В книге Рональда В. (ред.). Методы переписывания и приложения, 4-я международная конференция, RTA-91 . LNCS. Том 488. Springer. стр. 200–214.
• Тобиас Нипков (1991). «Критические пары высшего порядка». Труды 6-го симпозиума IEEE по логике в компьютерных науках . С. 342–349.
• Нипков, Т. (1995). "Системы переписывания высшего порядка (приглашенная лекция)". В Hsiang, Jieh (ред.). 6-я Международная конференция по методам и приложениям переписывания (RTA) . LNCS. Т. 914. Springer. стр. 256.
• Франц Баадер и Тобиас Нипков (1998). Переписывание терминов и все такое . Кембридж: Cambridge University Press. ISBN 978-0-521-45520-6.
• Нипков, Тобиас, ред. (1998). Методы переписывания и их применение, 9-я международная конференция, RTA-98 . LNCS. Том 1379. Springer.
• Нипков Т., Полсон Л. и Венцель М. (2002). Isabelle/HOL — помощник доказательства для логики высшего порядка . Springer.
• Gerwin Klein & Tobias Nipkow (2006). «Проверенная машиной модель для языка, подобного Java, виртуальная машина и компилятор». Труды ACM по языкам и системам программирования . 28 (4): 619–695. doi : 10.1145/1146809.1146811 .

Ссылки

1. Бланшетт, Жасмин (12 февраля 2021 г.). «Сообщение от нового главного редактора». Журнал автоматизированного рассуждения . 65 (2): 155. doi : 10.1007/s10817-021-09587-y . hdl : 1871.1/1216cab9-08c1-4d41-8069-aa1735f5786d .
2. Краткая биография
3. «Премия Эрбранда за выдающийся вклад в автоматизированное мышление». CADE Inc. Получено 14 июля 2021 г.
4. "Тобиас Нипков". Член . Academia Europaea . Получено 2024-10-03 .

Внешние ссылки

• Домашняя страница