Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

Partial Objects In Constructive Type Theory - Robert L. Constable; Scott F. Smith 001 (LICS, 1987)

Partial Objects in Type Theory. - Scott F. Smith 001 (1989)

Extracting Recursive Programs in Type Theory. - Scott F. Smith 001 (AMAST, 1991)

Reflective Semantics of Constructive Type Theory: Preliminary Report. - Scott F. Smith 001 (Constructivity in Computer Science, 1991)

From Operational to Denotational Semantics. - Scott F. Smith 001 (MFPS, 1991)

Towards a Theory of Actor Computation. - Gul Agha; Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (CONCUR, 1992)

A Theory of Classes for a Functional Language with Effects. - Furio Honsell; Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (CSL, 1992)

Provably Correct Synthesis of Asynchronous Circuits. - Scott F. Smith 001; Amy E. Zwarico (Designing Correct Circuits, 1992)

Computational Foundations of Basic Recursive Function Theory. - Robert L. Constable; Scott F. Smith 001 (Theor. Comput. Sci., 1993)

Application of OOP Type Theory: State, Decidability, Integragtion. - Jonathan Eifrig; Scott F. Smith 001; Valery Trifonov; Amy E. Zwarico (OOPSLA, 1994)

Sound Polymorphic Type Inference for Objects. - Jonathan Eifrig; Scott F. Smith 001; Valery Trifonov (OOPSLA, 1995)

Type inference for recursively constrained types and its application to OOP. - Jonathan Eifrig; Scott F. Smith 001; Valery Trifonov (MFPS, 1995)

Correct Compilation of Specifications to Deterministic Asynchronous Circuits. - Scott F. Smith 001; Amy E. Zwarico (Formal Methods Syst. Des., 1995)

Hybrid Partial-Total Type Theory. - Scott F. Smith 001 (Int. J. Found. Comput. Sci., 1995)

An Interpretation of Typed OOP in a Language with State. - Jonathan Eifrig; Scott F. Smith 001; Valery Trifonov; Amy E. Zwarico (LISP Symb. Comput., 1995)

On Binary Methods. - Kim B. Bruce; Luca Cardelli; Giuseppe Castagna; Jonathan Eifrig; Scott F. Smith 001; Valery Trifonov; Gary T. Leavens; Benjamin C. Pierce (Theory Pract. Object Syst., 1995)

A Variable Typed Logic of Effects - Furio Honsell; Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (Inf. Comput., 1995)

Subtyping Constrained Types. - Valery Trifonov; Scott F. Smith 001 (SAS, 1996)

From Operational Semantics to Domain Theory. - Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (Inf. Comput., 1996)

Constrained Types and Their Expressiveness. - Jens Palsberg; Scott F. Smith 001 (ACM Trans. Program. Lang. Syst., 1996)

A Foundation for Actor Computation. - Gul Agha; Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (J. Funct. Program., 1997)

Modular Reasoning for Actor Specification Diagrams. - Scott F. Smith 001; Carolyn L. Talcott (FMOODS, 1999)

Correspondence Polymorphism for Object-Oriented Languages. - Ran Rinat; Menachem Magidor; Scott F. Smith 001 (OOPSLA, 1999)

Polyvariant Flow Analysis with Constrained Types. - Scott F. Smith 001; Tiejun Wang (ESOP, 2000)

Static enforcement of security with types. - Christian Skalka; Scott F. Smith 001 (ICFP, 2000)

Precise Constraint-Based Type Inference for Java. - Tiejun Wang; Scott F. Smith 001 (ECOOP, 2001)

Modular Internet Programming with Cells. - Ran Rinat; Scott F. Smith 001 (ECOOP, 2002)

Set Types and Applications. - Christian Skalka; Scott F. Smith 001 (TIP@MPC, 2002)

Specification Diagrams for Actor Systems. - Scott F. Smith 001; Carolyn L. Talcott (High. Order Symb. Comput., 2002)

History Effects and Verification. - Christian Skalka; Scott F. Smith 001 (APLAS, 2004)

Modules with Interfaces for Dynamic Linking and Communication. - Yu David Liu; Scott F. Smith 001 (ECOOP, 2004)

Interaction-based programming with classages. - Yu David Liu; Scott F. Smith 001 (OOPSLA, 2005)

A Type and Effect System for Flexible Abstract Interpretation of Java: (Extended Abstract). - Christian Skalka; Scott F. Smith 001; David Van Horn (AIOOL@VMCAI, 2005)

Static use-based object confinement. - Christian Skalka; Scott F. Smith 001 (Int. J. Inf. Sec., 2005)

A systematic approach to static access control. - François Pottier; Christian Skalka; Scott F. Smith 001 (ACM Trans. Program. Lang. Syst., 2005)

A formal framework for component deployment. - Yu David Liu; Scott F. Smith 001 (OOPSLA, 2006)

A microkernel virtual machine: : building security with clear interfaces. - Xiaoqi Lu; Scott F. Smith 001 (PLAS, 2006)

Refactoring programs to secure information flows. - Scott F. Smith 001; Mark Thober (PLAS, 2006)

The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification. - Paritosh Shroff; Christian Skalka; Scott F. Smith 001 (APLAS, 2007)

Dynamic Dependency Monitoring to Secure Information Flow. - Paritosh Shroff; Scott F. Smith 001; Mark Thober (CSF, 2007)

Improving usability of information flow security in java. - Scott F. Smith 001; Mark Thober (PLAS, 2007)

Sound and Complete Type Inference for a Systems Programming Language. - Swaroop Sridhar; Jonathan S. Shapiro; Scott F. Smith 001 (APLAS, 2008)

Coqa: Concurrent Objects with Quantized Atomicity. - Yu David Liu; Xiaoqi Lu; Scott F. Smith 001 (CC, 2008)

Securing information flow via dynamic capture of dependencies. - Paritosh Shroff; Scott F. Smith 001; Mark Thober (J. Comput. Secur., 2008)

Types and trace effects of higher order programs. - Christian Skalka; Scott F. Smith 001; David Van Horn (J. Funct. Program., 2008)

Task types for pervasive atomicity. - Aditya Kulkarni; Yu David Liu; Scott F. Smith 001 (OOPSLA, 2010)

Backstage Java: making a difference in metaprogramming. - Zachary Palmer; Scott F. Smith 001 (OOPSLA, 2011)

Type-specialized staged programming with process separation. - Yu David Liu; Christian Skalka; Scott F. Smith 001 (High. Order Symb. Comput., 2011)

Scalaness/nesT: type specialized staged programming for sensor networks. - Peter C. Chapin; Christian Skalka; Scott F. Smith 001; Michael Watson (GPCE, 2013)

Types for Flexible Objects. - Zachary Palmer; Pottayil Harisanker Menon; Alexander Rozenshteyn; Scott F. Smith 001 (APLAS, 2014)

Higher-Order Demand-Driven Program Analysis. - Zachary Palmer; Scott F. Smith 001 (ECOOP, 2016)

CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond). - Kenneth Roe; Scott F. Smith 001 (ITP, 2016)

Higher-Order Demand-Driven Program Analysis (Artifact). - Leandro Facchinetti; Zachary Palmer; Scott F. Smith 001 (Dagstuhl Artifacts Ser., 2016)

Using the coq theorem prover to verify complex data structure invariants. - Kenneth Roe; Scott F. Smith 001 (MEMOCODE, 2017)

Relative Store Fragments for Singleton Abstraction. - Leandro Facchinetti; Zachary Palmer; Scott F. Smith 001 (SAS, 2017)

Higher-order Demand-driven Program Analysis. - Leandro Facchinetti; Zachary Palmer; Scott F. Smith 001 (ACM Trans. Program. Lang. Syst., 2019)

A Set-Based Context Model for Program Analysis. - Leandro Facchinetti; Zachary Palmer; Scott F. Smith 001; Ke Wu; Ayaka Yorihiro (APLAS, 2020)

Higher-order demand-driven symbolic evaluation. - Zachary Palmer; Theodore Park; Scott F. Smith 001; Shiwei Weng (Proc. ACM Program. Lang., 2020)

Semantic-Type-Guided Bug Finding. - Kelvin Qian; Scott F. Smith 001; Brandon Stride; Shiwei Weng; Ke Wu (Proc. ACM Program. Lang., 2024)

A Pure Demand Operational Semantics with Applications to Program Analysis. - Scott F. Smith 001; Robert Zhang 003 (Proc. ACM Program. Lang., 2024)