Nicolas Tabareau

Proceedings of the Programming Languages and Systems, 2024

2023

Impredicative Observational Equality.

[BibT_eX]

[DOI]

Loïc Pujet

Proc. ACM Program. Lang., January, 2023

2022

Gradualizing the Calculus of Inductive Constructions.

[BibT_eX]

[DOI]

Meven Lennon-Bertrand

Kenji Maillard

ACM Trans. Program. Lang. Syst., 2022

Observational equality: now for good.

[BibT_eX]

[DOI]

Loïc Pujet

Proc. ACM Program. Lang., 2022

A reasonably gradual type theory.

[BibT_eX]

[DOI]

Kenji Maillard

Meven Lennon-Bertrand

Proc. ACM Program. Lang., 2022

2021

The taming of the rew: a type theory with computational assumptions.

[BibT_eX]

[DOI]

Jesper Cockx

Théo Winterhalter

Proc. ACM Program. Lang., 2021

Model structure on the universe of all types in interval type theory.

[BibT_eX]

[DOI]

Simon Boulier

Math. Struct. Comput. Sci., 2021

The Marriage of Univalence and Parametricity.

[BibT_eX]

[DOI]

J. ACM, 2021

The Multiverse: Logical Modularity for Proof Assistants.

[BibT_eX]

[DOI]

CoRR, 2021

2020

Coq Coq correct! verification of type checking and erasure for Coq, in Coq.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

The fire triangle: how to mix substitution, dependent elimination, and effects.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

The MetaCoq Project.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

2019

A reasonably exceptional type theory.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Definitional proof-irrelevance without K.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations.

[BibT_eX]

[DOI]

Peter LeFanu Lumsdaine

J. Autom. Reason., 2019

Chemical foundations of distributed aspects.

[BibT_eX]

[DOI]

Distributed Comput., 2019

Setoid Type Theory - A Syntactic Translation.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Eliminating reflection from type theory.

[BibT_eX]

[DOI]

Théo Winterhalter

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Equivalences for free: univalent parametricity for effective transport.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

An explicit formula for the free exponential modality of linear logic.

[BibT_eX]

[DOI]

Christine Tasson

Math. Struct. Comput. Sci., 2018

Foundations of dependent interoperability.

[BibT_eX]

[DOI]

Pierre-Évariste Dagand

J. Funct. Program., 2018

Towards Certified Meta-Programming with Typed Template-Coq.

[BibT_eX]

[DOI]

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

Failure is Not an Option - An Exceptional Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

2017

An effectful way to eliminate addiction to dependence.

[BibT_eX]

[DOI]

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

The next 700 syntactical models of type theory.

[BibT_eX]

[DOI]

Simon Boulier

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Effect capabilities for Haskell: Taming effect interference in monadic programming.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2016

Lawvere-Tierney sheafification in Homotopy Type Theory.

[BibT_eX]

[DOI]

Kevin Quirin

J. Formaliz. Reason., 2016

The Definitional Side of the Forcing.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Partial type equivalences for verified dependent interoperability.

[BibT_eX]

[DOI]

Pierre-Évariste Dagand

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015

Wild omega-Categories for the Homotopy Hypothesis in Type Theory.

[BibT_eX]

[DOI]

André Hirschowitz

Tom Hirschowitz

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

Gradual certified programming in Coq.

[BibT_eX]

[DOI]

Proceedings of the 11th Symposium on Dynamic Languages, 2015

Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques.

[BibT_eX]

[DOI]

Guilhem Jaber

Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

2014

Execution levels for aspect-oriented programming: Design, semantics, implementations and applications.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

Effect Capabilities for Haskell.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages - 18th Brazilian Symposium, 2014

Lazier Imperative Programming.

[BibT_eX]

[DOI]

Rémi Douence

Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

Universe Polymorphism in Coq.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Aspectual session types.

[BibT_eX]

[DOI]

Mario Südholt

Proceedings of the 13th International Conference on Modularity, 2014

Compositional reasoning about aspect interference.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Modularity, 2014

2013

Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice.

[BibT_eX]

[DOI]

LNCS Trans. Aspect Oriented Softw. Dev., 2013

Taming aspects with monads and membranes.

[BibT_eX]

[DOI]

Proceedings of the 12th Workshop on Foundations of Aspect-Oriented Languages, 2013

A typed monadic embedding of aspects.

[BibT_eX]

[DOI]

Proceedings of the Aspect-Oriented Software Development, 2013

2012

Extending Type Theory with Forcing.

[BibT_eX]

[DOI]

Guilhem Jaber

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Taming aspects with membranes.

[BibT_eX]

[DOI]

Rémi Douence

Proceedings of the eleventh workshop on Foundations of Aspect-Oriented Languages, 2012

A practical monadic aspect weaver.

[BibT_eX]

[DOI]

Proceedings of the eleventh workshop on Foundations of Aspect-Oriented Languages, 2012

A monadic interpretation of execution levels and exceptions for AOP.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Aspect-oriented Software Development, 2012

2011

Aspect oriented programming: a language for 2-categories.

[BibT_eX]

[DOI]

Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, 2011

2010

How Synchronization Protects from Noise.

[BibT_eX]

[DOI]

Quang-Cuong Pham

PLoS Comput. Biol., 2010

Resource modalities in tensor logic.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2010

A theory of distributed aspects.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Aspect-Oriented Software Development, 2010

2009

A Contraction Theory Approach to Stochastic Incremental Stability.

[BibT_eX]

[DOI]

Quang-Cuong Pham

IEEE Trans. Autom. Control., 2009

An Algebraic Account of References in Game Semantics.

[BibT_eX]

[DOI]

Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics, 2009

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

[BibT_eX]

[DOI]

Nick Benton

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

2008

Modalités de ressource et contrôle en logique tensorielle. (Resource modalities and control in tensorial logic).

[BibT_eX]

[DOI]

PhD thesis, 2008

Where neuroscience and dynamic system theory meet autonomous robotics: A contracting basal ganglia model for action selection.

[BibT_eX]

[DOI]

Neural Networks, 2008

2007

Geometry of the superior colliculus mapping and efficient oculomotor computation.

[BibT_eX]

[DOI]

Daniel Bennequin

Alain Berthoz

Benoît Girard

Biol. Cybern., 2007

Resource modalities in game semantics.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006

De l'oprateur de trace dans les jeux de Conway

[BibT_eX]

[DOI]

CoRR, 2006

Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head.

[BibT_eX]

[DOI]

Proceedings of the 2006 6th IEEE-RAS International Conference on Humanoid Robots, 2006

2004

On Timed Automata with Input-Determined Guards.

[BibT_eX]

[DOI]

Deepak D'Souza