Lambda-Prolog: An Extended Logic Programming Language. - Amy P. Felty; Elsa L. Gunter; John Hannan; Dale Miller 001; Gopalan Nadathur; Andre Scedrov (CADE, 1988)

Extensions to Logic Programming Motivated by the Construction of a Generic Theorem Prover. - Elsa L. Gunter (ELP, 1989)

Pseudo-Retract Functors for Local Lattices and Bifinite L-domains. - Elsa L. Gunter (Mathematical Foundations of Programming Semantics, 1989)

Tutorial on Lambda-Prolog. - Amy P. Felty; Elsa L. Gunter; Dale Miller 001; Frank Pfenning (CADE, 1990)

An Abstract Interpretation for ML Equality Kinds. - Carl A. Gunter; Elsa L. Gunter; David B. MacQueen (TACS, 1991)

Implementing a Real-Time Process Algebra in HOL. - Richard Gerber 001; Elsa L. Gunter; Insup Lee 001 (TPHOLs, 1991)

Why we can't have SML-style datatype Declarations in HOL. - Elsa L. Gunter (TPHOLs, 1992)

A Broader Class of Trees for Recursive Type Definitions for HOL. - Elsa L. Gunter (HUG, 1993)

HOL-ML. - Myra Van Inwegen; Elsa L. Gunter (HUG, 1993)

Computing ML Equality Kinds Using Abstract Interpretation - Carl A. Gunter; Elsa L. Gunter; David B. MacQueen (Inf. Comput., 1993)

OR-SML: A Functional Database Programming Language for Disjunctive Information and Its Applications. - Elsa L. Gunter; Leonid Libkin (DEXA, 1994)

Interfacing HOL90 with a Functional Database Query Language. - Elsa L. Gunter; Leonid Libkin (TPHOLs, 1995)

Studying the ML Module System in HOL. - Elsa L. Gunter; Savi Maharaj (Comput. J., 1995)

The Village Telephone System: A Case Study in Formal Software Engineering. - Karthikeyan Bhargavan; Carl A. Gunter; Elsa L. Gunter; Michael Jackson 001; Davor Obradovic; Pamela Zave (TPHOLs, 1998)

Adding External Decision Procedures to HOL90 Securely. - Elsa L. Gunter (TPHOLs, 1998)

Path Exploration Tool. - Elsa L. Gunter; Doron A. Peled (TACAS, 1999)

PET: An Interactive Software Testing Tool. - Elsa L. Gunter; Robert P. Kurshan; Doron A. Peled (CAV, 2000)

A Reference Model for Requirements and Specifications-Extended Abstract. - Carl A. Gunter; Elsa L. Gunter; Michael Jackson 001; Pamela Zave (ICRE, 2000)

Using a Mix of Languages in Formal Methods: The PET System. - Elsa L. Gunter; Doron A. Peled (PDPTA, 2000)

Formal software engineering. - Carl A. Gunter; Elsa L. Gunter; Pamela Zave (ACM SIGSOFT Softw. Eng. Notes, 2000)

A Reference Model for Requirements and Specifications. - Carl A. Gunter; Elsa L. Gunter; Michael Jackson 001; Pamela Zave (IEEE Softw., 2000)

Temporal Debugging for Concurrent Systems. - Elsa L. Gunter; Doron A. Peled (TACAS, 2002)

Tracing the executions of concurrent programs. - Elsa L. Gunter; Doron A. Peled (RV@FLoC, 2002)

Unit Checking: Symbolic Model Checking for a Unit of Code. - Elsa L. Gunter; Doron A. Peled (Verification: Theory and Practice, 2003)

Compositional message sequence charts. - Elsa L. Gunter; Anca Muscholl; Doron A. Peled (Int. J. Softw. Tools Technol. Transf., 2003)

Typechecking Safe Process Synchronization. - Eduardo Bonelli; Adriana B. Compagnoni; Elsa L. Gunter (FGUC, 2004)

Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System. - Rajeev Alur; David Arney; Elsa L. Gunter; Insup Lee 001; Jaime Lee; Wonhong Nam; Frederick Pearce; Stephen Van Albert; Jiaxiang Zhou (Int. J. Softw. Tools Technol. Transf., 2004)

Types for Security in a Mobile World. - Adriana B. Compagnoni; Elsa L. Gunter (TGC, 2005)

Model checking, testing and verification working together. - Elsa L. Gunter; Doron A. Peled (Formal Aspects Comput., 2005)

Correspondence assertions for process synchronization in concurrent communications. - Eduardo Bonelli; Adriana B. Compagnoni; Elsa L. Gunter (J. Funct. Program., 2005)

I-Living: An Open System Architecture for Assisted Living. - Qixin Wang; Wook Shin; Xue Liu 001; Zheng Zeng 001; Cham Oh; Bedoor K. AlShebli; Marco Caccamo; Carl A. Gunter; Elsa L. Gunter; Jennifer C. Hou; Karrie Karahalios; Lui Sha (SMC, 2006)

The Simplex Reference Model: Limiting Fault-Propagation Due to Unreliable Components in Cyber-Physical System Architectures. - Tanya L. Crenshaw; Elsa L. Gunter; Craig L. Robinson; Lui Sha; P. R. Kumar 001 (RTSS, 2007)

Secure Broadcast Ambients. - Elsa L. Gunter; Ayesha Yasmeen (Formal Aspects in Security and Trust, 2008)

Role-based access control for boxed ambients. - Adriana B. Compagnoni; Elsa L. Gunter; Philippe Bidinger (Theor. Comput. Sci., 2008)

Specifying and Analyzing Workflows for Automated Identification and Data Capture. - Elsa L. Gunter; Ayesha Yasmeen; Carl A. Gunter; Anh Nguyen (HICSS, 2009)

Theory support for weak higher order abstract syntax in Isabelle/HOL. - Elsa L. Gunter; Christopher J. Osborn; Andrei Popescu 001 (LFMTP, 2009)

Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. - Andrei Popescu 001; Elsa L. Gunter (FoSSaCS, 2010)

A Framework for Formal Verification of Compiler Optimizations. - William Mansky; Elsa L. Gunter (ITP, 2010)

Strong Normalization for System F by HOAS on Top of FOAS. - Andrei Popescu 001; Elsa L. Gunter; Christopher J. Osborn (LICS, 2010)

Recursion principles for syntax with bindings and substitution. - Andrei Popescu 001; Elsa L. Gunter (ICFP, 2011)

Automated framework for formal operator task analysis. - Ayesha Yasmeen; Elsa L. Gunter (ISSTA, 2011)

Toward a multi-method approach to formalizing human-automation interaction and human-human communications. - Ellen J. Bass; Matthew L. Bolton; Karen M. Feigh; Dennis Griffith; Elsa L. Gunter; William Mansky; John M. Rushby (SMC, 2011)

Robustness for protection envelopes with respect to human task variation. - Ayesha Yasmeen; Elsa L. Gunter (SMC, 2011)

Formal Modeling and Analysis for Interactive Hybrid Systems. - Ellen J. Bass; Karen M. Feigh; Elsa L. Gunter; John M. Rushby (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Formal analysis of safety-critical system simulations. - Ayesha Yasmeen; Karen M. Feigh; Gabriel Gelman; Elsa L. Gunter (ATACCS, 2012)

Using Locales to Define a Rely-Guarantee Temporal Logic. - William Mansky; Elsa L. Gunter (ITP, 2012)

LiquidPi: Inferrable Dependent Session Types. - Dennis Griffith; Elsa L. Gunter (NASA Formal Methods, 2013)

Symbolic Analysis Tools for CSP. - Liyi Li 002; Elsa L. Gunter; William Mansky (ICTAC, 2014)

Verifying Optimizations for Concurrent Programs. - William Mansky; Elsa L. Gunter (WPTE@RTA/TLCA, 2014)

Specifying and Executing Optimizations for Parallel Programs. - William Mansky; Dennis Griffith; Elsa L. Gunter (GRAPHITE, 2014)

Specifying and executing optimizations for generalized control flow graphs. - William Mansky; Elsa L. Gunter; Dennis Griffith; Michael D. Adams 001 (Sci. Comput. Program., 2016)

A Method to Translate Order-Sorted Algebras to Many-Sorted Algebras. - Liyi Li 002; Elsa L. Gunter (WPTE@FSCD, 2017)

IsaK-Static: A Complete Static Semantics of mathbb K. - Liyi Li 002; Elsa L. Gunter (FACS, 2018)

Using a Computer-based Testing Facility to Improve Student Learning in a Programming Languages and Compilers Course. - Terence Nip; Elsa L. Gunter; Geoffrey L. Herman; Jason W. Morphew; Matthew West 001 (SIGCSE, 2018)

Dynamic class initialization semantics: a jinja extension. - Susannah Mansky; Elsa L. Gunter (CPP, 2019)

K-LLVM: A Relatively Complete Semantics of LLVM IR. - Liyi Li 002; Elsa L. Gunter (ECOOP, 2020)

Safety of a Smart Classes-Used Regression Test Selection Algorithm. - Susannah Mansky; Elsa L. Gunter (LSFA, 2020)

Per-Location Simulation. - Liyi Li 002; Elsa L. Gunter (NFM, 2020)

A Complete Semantics of $ mathbb {K}$ and Its Translation to Isabelle. - Liyi Li 002; Elsa L. Gunter (ICTAC, 2021)