Kegan McIlwaine
Ph.D. Computer Science - University of Wyoming
https://orcid.org/0000-0002-7505-5108 Research Interests
- Session Types & Linear Logic
- Formal Methods
- Programming Languages
Papers
- Kegan McIlwaine. Contracts, Simulations, and Sessions: Formal Verification of Compilers, Smart Contracts, and Protocols. University of Wyoming, Ph.D. Dissertation.
- Kegan McIlwaine, James Caldwell. Verifying Smart Contract Transformations Using Bisimulations. FMBC 2025
- Kegan McIlwaine, James Caldwell. Developing Faustus: A Formally Verified Smart Contract Programming Language. Submitted to iFM 2023.
- Kegan McIlwaine, Stone Olguin, James Caldwell. Faustus: Adding Formally Verified Parameterized Abstractions to the Smart Contract Language Marlowe. Submitted to WTSC 2022.
Talks
- Contracts, Simulations, and Sessions: Formal Verification of Compilers, Smart Contracts, and Protocols. Ph.D. Defense. Slides.
- Using Bisimulation to Formally Verify the Correctness of Smart Contract Transformations. MWPLS 2024. Slides.
- Compact Representation of Very Large Inline Programs. Wyoming Computing Symposium 2023. Slides. Program.
Projects
- STILL: Session Types and Intuitionistic Linear Logic Theorem Prover
- Faustus Smart Contract Programming Language
Experience
- 2017 - Present
- Full Stack Web Development (Angular/Javascript, HTML/CSS, .NET, PostgreSQL)
- 2020 - Present
- Interactive Theorem Proving in Isabelle
- 2020 - Present
- Haskell Programming
- 2020 - Present
- AWS Infrastructure as Code with Terraform
Academic Work
- Principles of Programming Languages
- Teaching Assistant - Spring 2026
- Computability and Complexity
- Teaching Assistant - Spring 2026, Fall 2025, Spring 2022
- Lectures given: Rice's Theorem, DFA Pumping Lemma, regular expressions
- Functional Programming
- Teaching Assistant - Fall 2025
- Algorithms and Data Structures
- Teaching Assistant - Spring 2020
- Lectures given: Recursion and induction, merge sort, sorting time complexity
Fun
