Дейл Миллер (академический)
Дейл Миллер | |
|---|---|
| Национальность | Американский |
| Род занятий | Ученый-компьютерщик и автор |
| Академическое образование | |
| Образование | Бакалавр математики доктор философии Математика |
| Альма-матер | Колледж Ливанской долины Университет Карнеги-Меллон |
| Академическая работа | |
| Учреждения | Инрия Сакле |
Дейл Миллер — американский учёный-компьютерщик и писатель. Он является директором по исследованиям в Inria Saclay и одним из разработчиков λProlog языка программирования Abella и интерактивного средства доказательства теорем . [ 1 ] [ 2 ]
Миллер наиболее известен своими исследованиями по темам вычислительной логики , включая теорию доказательств , автоматизированные рассуждения и формализованную метатеорию . Он является соавтором книги «Программирование с использованием логики высшего порядка» . [ 3 ]
Миллер является членом Ассоциации вычислительной техники (ACM). [ 4 ] В течение двух сроков с 2009 по 2015 год был главным редактором журнала ACM Transactions on Computational Logic и занимает редакционную должность в журнале Journal of Automated Reasoning . [ 5 ]
Ранняя жизнь и образование
[ редактировать ]В 1973 году, будучи старшеклассником средней школы Аннвилл-Клеона , Миллер опубликовал сложную задачу (задача H-237) в журнале Fibonacci Quarterly , где его имя было неправильно прочитано как «Д.А. Миллин». [ 6 ] Предмет этой проблемы теперь известен как серия Миллина. со степенью бакалавра математики В 1978 году он окончил колледж Ливан-Вэлли и получил степень доктора философии. по математике в 1983 году под руководством Питера Б. Эндрюса . [ 7 ]
Карьера
[ редактировать ]Получив докторскую степень, Миллер начал свою академическую карьеру в качестве доцента в Пенсильванском университете в 1983 году и получил звание доцента в 1989 году. С 1997 по 2001 год он был заведующим кафедрой компьютерных наук и инженерии. в Пенсильванском государственном университете . Он был профессором Политехнической школы с 2002 по 2006 год. [ 8 ]
Переехав во Францию в 2002 году, он в настоящее время является директором по исследованиям в Inria Saclay и в течение 12 лет был научным руководителем группы «Парсифаль» в Inria Saclay. [ 9 ]
Исследовать
[ редактировать ]Исследования Миллера охватывают область вычислительной логики и фокусируются на теории доказательств, автоматизированных рассуждениях, теории объединения , операционной семантике и логическом программировании . [ 10 ] Он наиболее известен как один из разработчиков языка программирования λProlog и интерактивного средства доказательства теорем Abella. Помимо других наград, он получил две награды LICS «Испытание временем». [ 11 ] и расширенный грант ERC . [ 9 ]
Логическое программирование и формализованная метатеория
[ редактировать ]Миллер и Гопалан Надатур совместно разработали язык логического программирования λProlog, который основан на интуиционистской логике высшего порядка и стал первым языком программирования, напрямую поддерживающим синтаксис λ-дерева (также известный как абстрактный синтаксис высшего порядка ). С момента появления языка в 1985 году были созданы различные реализации, включая ELPI и Teyjus. [ 12 ]
Вместе с Алвеном Тиу Миллер расширил теорию доказательств для фиксированных точек и количественной оценки первого порядка, включив в нее синтаксис λ-дерева. Их анализ показал, что отрицание как неудача приводит к различению между родовой и универсальной количественной оценкой. Они ввели ∇-квантор для определения общего квантора. Их расширенная логическая система могла напрямую охватить многие аспекты проверки моделей и метатеоретические аспекты π-исчисления . [ 13 ]
Работая с Надатуром, Тиу, Эндрю Гачеком и Каустувом Чаудхури, Миллер помог разработать интерактивное средство доказательства теорем Abella. Поскольку это средство доказательства напрямую поддерживает синтаксис λ-дерева, его можно использовать для индуктивного и коиндуктивного рассуждения о синтаксических объектах, содержащих привязку. Это доказательство было успешно применено к формализованной метатеории λ-исчисления , π-исчисления и к языкам программирования, заданным с использованием операционной семантики. [ 14 ]
Вычислительная логика и теория доказательств
[ редактировать ]Миллер проводил исследования в области вычислительной логики и теории доказательств, уделяя особое внимание применению концепций теории доказательств к проблемам информатики. Он показал, что теория доказательств может обеспечить плодотворную основу для логического программирования в классической, интуиционистской и линейной логике . [ 15 ] Работая с Чаком Ляном, он помог разработать концепцию целенаправленного доказательства секвентивного исчисления . Этот особый стиль системы подтверждения был использован в качестве основы для его гранта ProofCert, выданного ERC в 2012 году, в котором можно было определить и немедленно внедрить широкий спектр форматов сертификатов подтверждения. [ 16 ]
Миллер также использовал линейную логику в информатике. В частности, он продемонстрировал применение линейной логики для анализа естественного языка , операционных семантических спецификаций, проверки моделей и спецификации систем доказательства для классической, интуиционистской и линейной логики. [ 17 ]
Миллер также писал об унификации выражений λ-исчисления, уделяя особое внимание трактовке такой унификации, когда она выполняется как с использованием кванторов существования, так и с универсальными кванторами, а также на выявлении фрагмента унификации шаблона унификации более высокого порядка. фрагмент, который сильно напоминает объединение первого порядка при обработке связующих по обычным правилам λ-конверсии. [ 18 ]
Награды и почести
[ редактировать ]- 1974 - Финалист 33-го конкурса научных талантов Westinghouse (ныне Regeneron Science Talent Search).
- 2011 – Премия LICS «Испытание временем», LICS [ 11 ]
- 2014 – Премия LICS «Испытание временем», LICS
- 2021 – Член Ассоциации вычислительной техники. [ 4 ]
- 2022 – Член Азиатско-Тихоокеанской ассоциации искусственного интеллекта (AAIA). [ 19 ]
- 2023 г. – со-лауреат премии Дова Габая в области логики и оснований за 2023 г. [ 20 ]
Личная жизнь
[ редактировать ]Миллер живет во Франции. Он женат на Катуссии Паламидесси , имеет двоих детей. [ 7 ]
Библиография
[ редактировать ]Книги
[ редактировать ]- Миллер Д. и Надатур Г. (2012) Программирование с использованием логики высшего порядка , ISBN 9780521879408, Cambridge University Press.
Избранные статьи
[ редактировать ]- Надатур Г. и Миллер Д. (1988). Обзор λProlog. Пятая Международная конференция по логическому программированию, 810–827.
- Миллер, Д. (1989). Логический анализ модулей в логическом программировании. Журнал логического программирования , 6 (1-2), 79–108.
- Миллер Д., Надатур Г., Пфеннинг Ф. и Скедров А. (1991). Единообразные доказательства как основа логического программирования. Анналы чистой и прикладной логики, 51 (1-2), 125–157.
- Миллер, Д. (1991). Язык логического программирования с лямбда-абстракцией, функциональными переменными и простой унификацией. Журнал логики и вычислений , 1 (4), 497–536.
- Миллер, Д. (1992). Унификация под смешанной приставкой. Журнал символических вычислений, 14 (4), 321–358.
- Ходас Дж. С. и Миллер Д. (1994). Логическое программирование во фрагменте интуиционистской линейной логики. Информация и вычисления, 110(2), 327–365.
- Миллер Д. и Тиу А. (2005). Теория доказательства для общих суждений. Транзакции ACM по вычислительной логике, 6 (4), 749–783.
- Лян К. и Миллер Д. (2009). Фокусировка и поляризация в линейной, интуиционистской и классической логике. Теоретическая информатика, 410 (46), 4747–4768.
- Гацек А., Миллер Д. и Надатур Г. (2011). Номинальная абстракция. Информация и вычисления 209(1), 48–73.
- Чихани З., Миллер Д. и Рено Ф. (2017). Семантическая основа для доказательства. Журнал автоматизированного рассуждения. 59(3) 287–330.
- Миллер, Д. (2022). Обзор теоретико-доказательных основ логического программирования. Теория и практика логического программирования, 22 (6), 859–904.
Ссылки
[ редактировать ]- ^ «Абелла: система рассуждений о реляционных спецификациях» .
- ^ «Краткая биография Дейла Миллера» . www.lix.polytechnique.fr .
- ^ «Программирование с использованием логики высшего порядка» . сайты.google.com .
- ^ Перейти обратно: а б «Пресс-релиз: ACM НАЗЫВАЕТ 71 стипендиата за достижения в области вычислительной техники, способствующие инновациям» (PDF) .
- ^ «Журнал автоматизированных рассуждений» . Спрингер .
- ^ «ПЕРСОНАЛЬНЫЕ ПРОБЛЕМЫ И РЕШЕНИЯ» (PDF) .
- ^ Перейти обратно: а б «Дейл Миллер: «Делаем доказательство универсальным» | Инрия» . www.inria.fr .
- ^ «Дейл Миллер — ПОПЛ 2023» . popl23.sigplan.org .
- ^ Перейти обратно: а б «Дейл Миллер | Инрия» . www.inria.fr .
- ^ «Дейл Миллер» . ученый.google.com .
- ^ Перейти обратно: а б «ЛИКС-Архив» . lics.siglog.org .
- ^ «Тейюс» .
- ^ Миллер, Дейл; Тиу, Алвен (1 октября 2005 г.). «Теория доказательства для общих суждений» . Транзакции ACM в вычислительной логике . 6 (4): 749–783. doi : 10.1145/1094622.1094628 – до октября 2005 г.
- ^ Бельде, Дэвид; Чаудхури, Каустув; Гацек, Эндрю; Миллер, Дейл; Надатур, Гопалан; Тиу, Алвен; Ван, Ютин (30 декабря 2014 г.). «Абелла: система рассуждений о реляционных спецификациях» . Журнал формализованного рассуждения . 7 (2): 1–89. doi : 10.6092/issn.1972-5787/4650 – через jfr.unibo.it.
- ^ Лян, Чак; Миллер, Дейл (1 ноября 2009 г.). «Фокусировка и поляризация в линейной, интуиционистской и классической логике» . Теоретическая информатика . 410 (46): 4747–4768. doi : 10.1016/j.tcs.2009.07.041 – через ScienceDirect.
- ^ Чихани, Закария; Миллер, Дейл; Рено, Фабьен (1 октября 2017 г.). «Семантическая основа доказательств» . Журнал автоматизированного рассуждения . 59 (3): 287–330. doi : 10.1007/s10817-016-9380-6 – через Springer Link.
- ^ Миллер, Дейл; Пиментел, Элейн (24 февраля 2002 г.). Эгли, Уве; Фермюллер, Кристиан Г. (ред.). «Использование линейной логики для рассуждений о секвенционных системах» . Спрингер. стр. 2–23. doi : 10.1007/3-540-45616-3_2 – через Springer Link.
- ^ «Язык логического программирования с лямбда-абстракцией, функциональными переменными и простой унификацией» .
- ^ «Азиатско-Тихоокеанская ассоциация искусственного интеллекта» . aaia-ai.org .
- ^ https://iloaf.org/dgp-ceremony-2023.html
| Международный | |
|---|---|
| Национальный | |
| академики | |
| Другой | |
