Jacques Garrigue

According to our database, Jacques Garrigue authored at least 33 papers between 1994 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

An intuitionistic set-theoretical model of fully dependent CC.

Masahiro Sato, Jacques Garrigue

Math. Struct. Comput. Sci., 2023

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

CoRR, 2023

Typed compositional quantum computation with lenses.

Jacques Garrigue, Takafumi Saikawa

CoRR, 2023

2021

A trustful monad for axiomatic reasoning with probability and nondeterminism.

Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa

J. Funct. Program., 2021

2020

A Library for Formalization of Linear Error-Correcting Codes.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

J. Autom. Reason., 2020

An Intuitionistic Set-theoretical Model of Fully Dependent CCω.

Masahiro Sato, Jacques Garrigue

CoRR, 2020

Formal Adventures in Convex and Conical Spaces.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019

Lightweight Linearly-typed Programming with Lenses and Monads.

Keigo Imai, Jacques Garrigue

J. Inf. Process., 2019

Proving Tree Algorithms for Succinct Data Structures.

Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Safe Low-level Code Generation in Coq Using Monomorphization and Monadification.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue

J. Inf. Process., 2018

Examples of Formal Proofs about Data Compression.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Proceedings of the International Symposium on Information Theory and Its Applications, 2018

2016

An Intuitionistic Set-theoretical Model of CC^<i>ω</i>.

Masahiro Sato, Jacques Garrigue

J. Inf. Process., 2016

Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Proceedings of the 2016 International Symposium on Information Theory and Its Applications, 2016

Formal Verification of the rank Algorithm for Succinct Data Structures.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue

Proceedings of the Formal Methods and Software Engineering, 2016

2015

A certified implementation of ML with structural polymorphism and recursive types.

Jacques Garrigue

Math. Struct. Comput. Sci., 2015

GADTs and Exhaustiveness: Looking for the Impossible.

Jacques Garrigue, Jacques Le Normand

Proceedings of the Proceedings ML Family / OCaml Users and Developers workshops, 2015

Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory.

Reynald Affeldt, Jacques Garrigue

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Summer School on Coq (NII Shonan Meeting 2014-9).

Pierre Castéran, Jacques Garrigue, David Nowak

NII Shonan Meet. Rep., 2014

2013

Ambivalent Types for Principal Type Inference with GADTs.

Jacques Garrigue, Didier Rémy

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

2011

Path resolution for nested recursive modules.

Jacques Garrigue, Keiko Nakata

High. Order Symb. Comput., 2011

A syntactic type system for recursive modules.

Hyeonseung Im, Keiko Nakata, Jacques Garrigue, Sungwoo Park

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

2010

A Certified Implementation of ML with Structural Polymorphism.

Jacques Garrigue

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2006

Recursive modules for programming.

Keiko Nakata, Jacques Garrigue

Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006

Private Row Types: Abstracting the Unnamed.

Jacques Garrigue

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

2005

SOBA Framework: An Application Framework for Broadband Network Environment.

Nobuaki Yoshida, Yoshio Hayashi, Yutaka Tamagaki, Shoji Urashita, Makoto Kakuta, Masahiro Watanabe, Jacques Garrigue, Reiji Nakajima

Proceedings of the 2005 IEEE/IPSJ International Symposium on Applications and the Internet (SAINT 2005), 31 January, 2005

2002

Relaxing the Value Restriction.

Jacques Garrigue

Proceedings of the Third Asian Workshop on Programming Languages and Systems, 2002

2001

Simple Type Inference for Structural Polymorphism.

Jacques Garrigue

Proceedings of the Second Asian Workshop on Programming Languages and Systems, 2001

1999

Semi-Explicit First-Class Polymorphism for ML.

Jacques Garrigue, Didier Rémy

Inf. Comput., 1999

1998

On the Runtime Complexity of Type-Directed Unboxing.

Yasuhiko Minamide, Jacques Garrigue

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

1997

Extending ML with Semi-Explicit Higher-Order Polymorphism.

Jacques Garrigue, Didier Rémy

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

1995

Label-Selective lambda-Calculus Syntax and Confluence.

Hassan Aït-Kaci, Jacques Garrigue

Theor. Comput. Sci., 1995

The Transformation Calculus.

Jacques Garrigue

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

1994

The Typed Polymorphic Label-Selective lambda-Calculus.

Jacques Garrigue, Hassan Aït-Kaci

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