Robert Harper

CoRR, 2024

Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory.

[BibT_eX]

[DOI]

Yue Niu

CoRR, 2024

2023

A Verified Cost Analysis of Joinable Red-Black Trees.

[BibT_eX]

[DOI]

Runming Li

CoRR, 2023

Logical Relations for Session-Typed Concurrency.

[BibT_eX]

[DOI]

CoRR, 2023

Amortized Analysis via Coinduction.

[BibT_eX]

[DOI]

CoRR, 2023

A Metalanguage for Cost-Aware Denotational Semantics.

[BibT_eX]

[DOI]

Yue Niu

Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, 2023

Amortized Analysis via Coinduction (Early Ideas).

[BibT_eX]

[DOI]

Proceedings of the 10th Conference on Algebra and Coalgebra in Computer Science, 2023

Integrating Cost and Behavior in Type Theory (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 10th Conference on Algebra and Coalgebra in Computer Science, 2023

2022

A cost-aware logical framework.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Sheaf Semantics of Termination-Insensitive Noninterference.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

Syntax and models of Cartesian cubical type theory.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2021

Internal Parametricity for Cubical Type Theory.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules.

[BibT_eX]

[DOI]

J. ACM, 2021

An Equational Logical Framework for Type Theories.

[BibT_eX]

[DOI]

CoRR, 2021

2020

The history of Standard ML.

[BibT_eX]

[DOI]

David MacQueen

John H. Reppy

Proc. ACM Program. Lang., 2020

Cost-Aware Type Theory.

[BibT_eX]

[DOI]

Yue Niu

CoRR, 2020

2019

A separation logic for concurrent randomized programs.

[BibT_eX]

[DOI]

Joseph Tassarotti

Proc. ACM Program. Lang., 2019

Higher inductive types in cubical computational type theory.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Parametric Cubical Type Theory.

[BibT_eX]

[DOI]

CoRR, 2019

2018

Exception tracking in an open world.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2018

Competitive parallelism: getting your priorities right.

[BibT_eX]

[DOI]

Stefan K. Muller

Proc. ACM Program. Lang., 2018

The RedPRL Proof Assistant (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2018

Computational Higher Type Theory IV: Inductive Types.

[BibT_eX]

[DOI]

CoRR, 2018

Guarded Computational Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Verified Tail Bounds for Randomized Programs.

[BibT_eX]

[DOI]

Joseph Tassarotti

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.

[BibT_eX]

[DOI]

Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

2017

Correctness of compiling polymorphism to dynamic typing.

[BibT_eX]

[DOI]

Nick Benton

J. Funct. Program., 2017

Computational Higher Type Theory III: Univalent Universes and Exact Equality.

[BibT_eX]

[DOI]

CoRR, 2017

Algebraic Foundations of Proof Refinement.

[BibT_eX]

[DOI]

CoRR, 2017

Parallel functional arrays.

[BibT_eX]

[DOI]

Ananya Kumar

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Computational higher-dimensional type theory.

[BibT_eX]

[DOI]

Todd Wilson

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Responsive parallel computation: bridging competitive and cooperative threading.

[BibT_eX]

[DOI]

Stefan K. Muller

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

A Higher-Order Logic for Concurrent Termination-Preserving Refinement.

[BibT_eX]

[DOI]

Joseph Tassarotti

Ralf Jung

Proceedings of the Programming Languages and Systems, 2017

2016

Homotopical patch theory.

[BibT_eX]

[DOI]

J. Funct. Program., 2016

Computational Higher Type Theory II: Dependent Cubical Realizability.

[BibT_eX]

[DOI]

CoRR, 2016

Computational Higher Type Theory I: Abstract Cubical Realizability.

[BibT_eX]

[DOI]

Todd Wilson

CoRR, 2016

Covering Spaces in Homotopy Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

Practical Foundations for Programming Languages (2nd. Ed.).

[BibT_eX]

[DOI]

Cambridge University Press, ISBN: 9781107150300, 2016

2015

Homotopy type theory: unified foundations of mathematics and computation.

[BibT_eX]

[DOI]

Steve Awodey

ACM SIGLOG News, 2015

A Note on the Uniform Kan Condition in Nominal Cubical Sets.

[BibT_eX]

[DOI]

CoRR, 2015

Cache efficient functional algorithms.

[BibT_eX]

[DOI]

Commun. ACM, 2015

2013

Cache and I/O efficent functional algorithms.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2012

Canonicity for 2-dimensional type theory.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

2-Dimensional Directed Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

Robin Milner 1934--2010: verification, languages, and concurrency.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

2010

Space profiling for parallel functional programs.

[BibT_eX]

[DOI]

J. Funct. Program., 2010

A Monadic Formalization of ML5

[BibT_eX]

[DOI]

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Distributed programming with distributed authorization.

[BibT_eX]

[DOI]

Kumar Avijit

Anupam Datta

Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2010

2009

An experimental analysis of self-adjusting computation.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2009

An overview of the Oregon programming languages summer school.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 2009

FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum.

[BibT_eX]

[DOI]

J. Funct. Program., 2009

A Pronominal Approach to Binding and Computation.

[BibT_eX]

[DOI]

Noam Zeilberger

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures.

[BibT_eX]

[DOI]

Proceedings of the SPAA 2009: Proceedings of the 21st Annual ACM Symposium on Parallelism in Algorithms and Architectures, 2009

Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report.

[BibT_eX]

[DOI]

Proceedings of the 40th SIGCSE Technical Symposium on Computer Science Education, 2009

Positively dependent types.

[BibT_eX]

[DOI]

Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, 2009

A universe of binding and computation.

[BibT_eX]

[DOI]

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008

Position paper: practical foundations for lrogramming languages.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 2008

SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations.

[BibT_eX]

[DOI]

Shriram Krishnamurthi

ACM SIGPLAN Notices, 2008

Focusing on Binding and Computation.

[BibT_eX]

[DOI]

Noam Zeilberger

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

2007

Mechanizing metatheory in a logical framework.

[BibT_eX]

[DOI]

J. Funct. Program., 2007

Syntactic Logical Relations for Polymorphic and Recursive Types.

[BibT_eX]

[DOI]

Proceedings of the Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, 2007

Type-Safe Distributed Programming with ML5.

[BibT_eX]

[DOI]

Tom Murphy VII

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Towards a mechanized metatheory of standard ML.

[BibT_eX]

[DOI]

Daniel K. Lee

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Modular type classes.

[BibT_eX]

[DOI]

Derek Dreyer

Manuel M. T. Chakravarty

Gabriele Keller

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

2006

Adaptive functional programming.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2006

Extensional equivalence and singleton types.

[BibT_eX]

[DOI]

Christopher A. Stone

ACM Trans. Comput. Log., 2006

Higher-order abstract syntax: setting the record straight.

[BibT_eX]

[DOI]

SIGACT News, 2006

Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight

[BibT_eX]

[DOI]

CoRR, 2006

A separate compilation extension to standard ML.

[BibT_eX]

[DOI]

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

2005

On equivalence and canonical forms in the LF type theory.

[BibT_eX]

[DOI]

Frank Pfenning

ACM Trans. Comput. Log., 2005

A Library for Self-Adjusting Computation.

[BibT_eX]

[DOI]

Proceedings of the ACM-SIGPLAN Workshop on ML, 2005

Using page residency to balance tradeoffs in tracing garbage collection.

[BibT_eX]

[DOI]

Daniel Spoonhower

Proceedings of the 1st International Conference on Virtual Execution Environments, 2005

Strict bidirectional type checking.

[BibT_eX]

[DOI]

Adam Chlipala

Leaf Petersen

Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Mechanizing the meta-theory of programming languages.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

Distributed Control Flow with Classical Modal Logic.

[BibT_eX]

[DOI]

Tom Murphy VII

Proceedings of the Computer Science Logic, 19th International Workshop, 2005

2004

Editorial.

[BibT_eX]

[DOI]

David A. Basin

Olivier Danvy

High. Order Symb. Comput., 2004

Dynamizing static algorithms, with applications to dynamic trees and history independence.

[BibT_eX]

[DOI]

Shan Leung Maverick Woo

Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, 2004

A Symmetric Modal Lambda Calculus for Distributed Computing.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Self-Adjusting Computation.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Self-adjusting beat detection and prediction in music.

[BibT_eX]

[DOI]

M. Ed Jernigan

Proceedings of the 2004 IEEE International Conference on Acoustics, 2004

2003

Automated techniques for provably safe mobile code.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Automatic Generation of Staged Geometric Predicates.

[BibT_eX]

[DOI]

Aleksandar Nanevski

High. Order Symb. Comput., 2003

Typed compilation of recursive datatypes.

[BibT_eX]

[DOI]

Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

A type theory for memory allocation and data layout.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

A type system for higher-order modules.

[BibT_eX]

[DOI]

Derek Dreyer

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

Selective memoization.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

An effective theory of type refinements.

[BibT_eX]

[DOI]

Yitzhak Mandelbaum

David Walker

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

2002

Trustless Grid Computing in ConCert.

[BibT_eX]

[DOI]

Proceedings of the Grid Computing, 2002

2001

A Network Protocol Stack in Standard ML.

[BibT_eX]

[DOI]

Edoardo Biagioni

High. Order Symb. Comput., 2001

Persistent triangulations Journal of Functional Programming.

[BibT_eX]

[DOI]

J. Funct. Program., 2001

On the unusual effectiveness of logic in computer science.

[BibT_eX]

[DOI]

Bull. Symb. Log., 2001

A Dependently Typed Assembly Language.

[BibT_eX]

[DOI]

Hongwei Xi

Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), 2001

A Language-Based Approach to Security.

[BibT_eX]

[DOI]

Fred B. Schneider

Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

2000

Deciding Type Equivalence with Singleton Kinds.

[BibT_eX]

[DOI]

Christopher A. Stone

Proceedings of the POPL 2000, 2000

Advanced module systems: a guide for the perplexed (abstract of invited talk).

[BibT_eX]

[DOI]

Benjamin C. Pierce

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

A type-theoretic interpretation of standard ML.

[BibT_eX]

Christopher A. Stone

Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999

Proof-Directed Debugging.

[BibT_eX]

[DOI]

J. Funct. Program., 1999

Parametricity and Variants of Girard's <i>J</i> Operator.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1999

Relational Interpretations of Recursive Types in an Operational Setting.

[BibT_eX]

[DOI]

Lars Birkedal

Inf. Comput., 1999

What is a Recursive Module?

[BibT_eX]

[DOI]

Sidd Puri

Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1999

1998

A Module System for a Programming Language Based on the LF Logical Framework.

[BibT_eX]

[DOI]

Frank Pfenning

J. Log. Comput., 1998

How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler.

[BibT_eX]

[DOI]

Andrew Bernard

Proceedings of the Types in Compilation, Second International Workshop, 1998

Generational Stack Collection and Profile-Driven Pretenuring.

[BibT_eX]

[DOI]

Perry Cheng

Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI), 1998

1997

Typed Closure Conversion for Recursively-Defined Functions.

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

Relational Interpretations of Recursive Types in an operational Setting (Summary).

[BibT_eX]

[DOI]

Lars Birkedal

Proceedings of the Theoretical Aspects of Computer Software, Third International Symposium, 1997

1996

Operational Interpretations of an Extension of F<sub>omega</sub> with Control Operators.

[BibT_eX]

[DOI]

J. Funct. Program., 1996

A Note on "A Simplified Account of Polymorphic References".

[BibT_eX]

[DOI]

Inf. Process. Lett., 1996

ML and Beyond.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

Research in Programming Languages for Composability, Safety, and Performance.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

Typed Closure Conversion.

[BibT_eX]

[DOI]

Yasuhiko Minamide

Proceedings of the Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1996

TIL: a type-directed, optimizing compiler for ML (with retrospective)

[BibT_eX]

[DOI]

Proceedings of the 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, 1996

TIL: A Type-Directed Optimizing Compiler for ML.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI), 1996

1995

Compiling Polymorphism Using Intensional Type Analysis.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

Abstract Models of Memory Management.

[BibT_eX]

[DOI]

Matthias Felleisen

Proceedings of the seventh international conference on Functional programming languages and computer architecture, 1995

1994

A Simplified Account of Polymorphic References.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1994

Structured Theory Presentations and Logic Representations.

[BibT_eX]

[DOI]

Donald Sannella

Andrzej Tarlecki

Ann. Pure Appl. Log., 1994

A Type-Theoretic Approach to Higher-Order Modules with Sharing.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994

Signatures for a Network Protocol Stack: A Systems Application of Standard ML.

[BibT_eX]

[DOI]

Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

1993

On the Type Structure of Standard ML.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 1993

Polymorphic Type Assignment and CPS Conversion.

[BibT_eX]

LISP Symb. Comput., 1993

Typing First-Class Continuations in ML.

[BibT_eX]

[DOI]

Bruce F. Duba

David B. MacQueen

J. Funct. Program., 1993

A Framework for Defining Logics.

[BibT_eX]

[DOI]

Furio Honsell

Gordon D. Plotkin

J. ACM, 1993

Explicit Polymorphism and CPS Conversion.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

1992

Constructing Type Systems over an Operational Semantics.

[BibT_eX]

[DOI]

J. Symb. Comput., 1992

1991

Type Checking with Universes.

[BibT_eX]

[DOI]

Robert Pollack

Theor. Comput. Sci., 1991

A Record Calculus Based on Symmetric Concatenation.

[BibT_eX]

[DOI]

Benjamin C. Pierce

Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

1990

Higher-Order Modules and the Phase Distinction.

[BibT_eX]

[DOI]

Eugenio Moggi

Proceedings of the Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1990

Definition of standard ML.

[BibT_eX]

Robin Milner

Mads Tofte

MIT Press, ISBN: 978-0-262-63132-7, 1990

1989

Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft).

[BibT_eX]

[DOI]

Robert Pollack

Proceedings of the TAPSOFT'89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1989

Structure and Representation in LF

[BibT_eX]

[DOI]

Donald Sannella

Andrzej Tarlecki

Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

Logic Representation in LF.

[BibT_eX]

[DOI]

Donald Sannella

Andrzej Tarlecki

Proceedings of the Category Theory and Computer Science, 1989

1988

The Essence of ML.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988

1987

A Type Discipline for Program Modules.

[BibT_eX]

[DOI]

Robin Milner

Mads Tofte

Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

1986

Implementing mathematics with the Nuprl proof development system.

[BibT_eX]

[DOI]

Prentice Hall, ISBN: 978-0-13-451832-9, 1986

1985

Aspects of the Implementation of Type Theory.

[BibT_eX]

PhD thesis, 1985

Modules and Persistence in Standard ML.

[BibT_eX]