Nick Benton

Martin Hofmann

Vivek Nigam

Sci. Comput. Program., 2018

Proof-Relevant Logical Relations for Name Generation.

[BibT_eX]

[DOI]

Martin Hofmann

Vivek Nigam

Log. Methods Comput. Sci., 2018

Semantic Equivalence Checking for HHVM Bytecode.

[BibT_eX]

[DOI]

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, 2018

2017

Correctness of compiling polymorphism to dynamic typing.

[BibT_eX]

[DOI]

Kuen-Bang Hou (Favonia)

Robert Harper

J. Funct. Program., 2017

2016

Counting Successes: Effects and Transformations for Non-deterministic Programs.

[BibT_eX]

[DOI]

Proceedings of the A List of Successes That Can Change the World, 2016

2015

Integrating Linear and Dependent Types.

[BibT_eX]

[DOI]

Cécilia Pradic

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

Abstract effects and proof-relevant logical relations.

[BibT_eX]

[DOI]

Martin Hofmann

Vivek Nigam

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

Coq: the world's best macro assembler?

[BibT_eX]

[DOI]

Jonas Braband Jensen

Pierre-Évariste Dagand

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

High-level separation logic for low-level code.

[BibT_eX]

[DOI]

Jonas Braband Jensen

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

The Proof Assistant as an Integrated Development Environment.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012

Strongly Typed Term Representations in Coq.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Higher-order functional reactive programming in bounded space.

[BibT_eX]

[DOI]

Jan Hoffmann

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

Adding Equations to System F Types.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2012

2011

Ultrametric Semantics of Reactive Programs.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

A semantic model for graphical user interfaces.

[BibT_eX]

[DOI]

Proceedings of the Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011

2010

Step-Indexing: The Good, the Bad and the Ugly.

[BibT_eX]

[DOI]

Chung-Kil Hur

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

10351 Executive Summary - Modelling, Controlling and Reasoning About State.

[BibT_eX]

[DOI]

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.

[BibT_eX]

[DOI]

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

2009

Some Domain Theory and Denotational Semantics in Coq.

[BibT_eX]

[DOI]

Carsten Varming

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Compiling functional types to relational specifications for low level imperative code.

[BibT_eX]

[DOI]

Nicolas Tabareau

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

Relational semantics for effect-based program transformations: higher-order store.

[BibT_eX]

[DOI]

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

Biorthogonality, step-indexing and compiler correctness.

[BibT_eX]

[DOI]

Chung-Kil Hur

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

2008

Undoing Dynamic Typing (Declarative Pearl).

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Diagrammatic Reasoning in Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Diagrammatic Representation and Inference, 5th International Conference, 2008

08061 Abstracts Collection -- Types, Logics and Semantics for State.

[BibT_eX]

[DOI]

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

08061 Executive Summary -- Types, Logics and Semantics for State.

[BibT_eX]

[DOI]

Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

2007

Semantics of an effect analysis for exceptions.

[BibT_eX]

[DOI]

Peter Buchlovsky

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

Formalizing and verifying semantic type soundness of a simple compiler.

[BibT_eX]

[DOI]

Uri Zarfaty

Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Relational semantics for effect-based program transformations with dynamic allocation.

[BibT_eX]

[DOI]

Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

2006

Abstracting Allocation.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 20th International Workshop, 2006

Reading, Writing and Relations.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

2005

Embedded interpreters.

[BibT_eX]

[DOI]

J. Funct. Program., 2005

Preface.

[BibT_eX]

[DOI]

Xavier Leroy

Proceedings of the ACM-SIGPLAN Workshop on ML, 2005

Relational Reasoning in a Nominal Semantics for Storage.

[BibT_eX]

[DOI]

Benjamin Leperchey

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

A Typed, Compositional Logic for a Stack-Based Abstract Machine.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2004

Modern concurrency abstractions for C#.

[BibT_eX]

[DOI]

Luca Cardelli

Cédric Fournet

ACM Trans. Program. Lang. Syst., 2004

Adventures in interoperability: the SML.NET experience.

[BibT_eX]

[DOI]

Claudio V. Russo

Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2004

Simple relational correctness proofs for static analyses and program transformations.

[BibT_eX]

[DOI]

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

Shrinking Reductions in SML.NET.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Functional Languages, 2004

2003

Traced Premonoidal Categories.

[BibT_eX]

[DOI]

Martin Hyland

RAIRO Theor. Informatics Appl., 2003

2002

Traced pre-monoidal categories.

[BibT_eX]

Martin Hyland

Proceedings of the Fixed Points in Computer Science, 2002

Modern Concurrency Abstractions for C<sup>#</sup>.

[BibT_eX]

[DOI]

Luca Cardelli

Cédric Fournet

Proceedings of the ECOOP 2002, 2002

2001

BABEL 2001 - Preface.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Multi-Language Infrastructure and Interoperability, 2001

Exceptional Syntax Journal of Functional Programming.

[BibT_eX]

[DOI]

J. Funct. Program., 2001

2000

Type inference for MLj.

[BibT_eX]

Bruce J. McAdam

Proceedings of the Selected papers from the 2nd Scottish Functional Programming Workshop (SFP00), 2000

Monads and Effects.

[BibT_eX]

[DOI]

John Hughes

Eugenio Moggi

Proceedings of the Applied Semantics, International Summer School, 2000

1999

Monads, Effects and Transformations.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Higher-Order Operational Techniques in Semantics, 1999

Interlanguage Working Without Tears: Blending SML with Java.

[BibT_eX]

[DOI]

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

1998

Computational Types from a Logical Perspective.

[BibT_eX]

[DOI]

Gavin M. Bierman

Valeria de Paiva

J. Funct. Program., 1998

Compiling Standard ML to Java Bytecodes.

[BibT_eX]

[DOI]

George Russell

Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

1996

On the Relationship Between Formal Semantics and Static Analysis.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

Linear Logic, Monads and the Lambda Calculus.

[BibT_eX]

[DOI]

Philip Wadler

Proceedings of the Proceedings, 1996

1995

Strong Normalisation for the Linear Term Calculus.

[BibT_eX]

[DOI]

J. Funct. Program., 1995

1994

A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1993

A Term Calculus for Intuitionistic Linear Logic.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

Strictness Properties of Lazy Algebraic Datatypes.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, Third International Workshop, 1993

1992

Strictness Logic and Polymorphic Invariance.

[BibT_eX]

[DOI]