Georges Gonthier

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

A Machine-Checked Proof of the Odd Order Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

A Language of Patterns for Subterm Selection.

[BibT_eX]

[DOI]

Enrico Tassi

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Type design patterns for computer mathematics.

[BibT_eX]

[DOI]

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

Point-Free, Set-Free Concrete Linear Algebra.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Advances in the Formalization of the Odd Order Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

An introduction to small scale reflection in Coq.

[BibT_eX]

[DOI]

Assia Mahboubi

J. Formaliz. Reason., 2010

2009

Packaging Mathematical Structures.

[BibT_eX]

[DOI]

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

Software Engineering for Mathematics.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

2008

Canonical Big Operators.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007

A Modular Formalisation of Finite Group Theory.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

The Four Colour Theorem: Engineering of a Formal Proof.

[BibT_eX]

[DOI]

Proceedings of the Computer Mathematics, 8th Asian Symposium, 2007

2006

Coq.

[BibT_eX]

[DOI]

Laurent Théry

Pierre Letouzey

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

A hierarchy of equivalences for asynchronous calculi.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2005

Using Stålmarck's Algorithm to Prove Inequalities.

[BibT_eX]

[DOI]

Byron Cook

Proceedings of the Formal Methods and Software Engineering, 2005

2004

Choice in Dynamic Linking.

[BibT_eX]

[DOI]

Benjamin Werner

Proceedings of the Foundations of Software Science and Computation Structures, 2004

2000

Authentication Primitives and Their Compilation.

[BibT_eX]

[DOI]

Proceedings of the POPL 2000, 2000

The Join Calculus: A Language for Distributed Mobile Programming.

[BibT_eX]

[DOI]

Proceedings of the Applied Semantics, International Summer School, 2000

1999

Secure Communications Processing for Distributed Languages.

[BibT_eX]

[DOI]

Proceedings of the 1999 IEEE Symposium on Security and Privacy, 1999

A Top-Down Look at a Secure Message.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1999

1997

Secure Implementation of Channel Abstractions.

[BibT_eX]

[DOI]

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

1996

The Reflexive CHAM and the Join-Calculus.

[BibT_eX]

[DOI]

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

A Calculus of Mobile Agents.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '96, 1996

Verifying the Safety of a Practical Concurrent Garbage Collector.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1994

Portable, Unobtrusive Garbage Collection for Multiprocessor Systems.

[BibT_eX]

[DOI]

Damien Doligez

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

1992

The Esterel Synchronous Programming Language: Design, Semantics, Implementation.

[BibT_eX]

[DOI]

Gérard Berry

Sci. Comput. Program., 1992

The Geometry of Optimal Lambda Reduction.

[BibT_eX]

[DOI]

Jean-Jacques Lévy

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

An abstract standardisation theorem

[BibT_eX]

[DOI]

Jean-Jacques Lévy

Paul-André Melliès

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

Linear Logic Without Boxes

[BibT_eX]

[DOI]

Jean-Jacques Lévy

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

1991

Incremental Development of an HDLC Entity in Esterel.

[BibT_eX]

[DOI]

Gérard Berry

Comput. Networks ISDN Syst., 1991

1985

Algebraic Calculi of Processes and Net Expressions.

[BibT_eX]

[DOI]