Jacques Garrigue

45 papers A* 1A 4B 9C 5Misc 2Journal 18Unranked 5

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A practical formalization of monadic equational reasoning in dependent-type theory. J. Funct. Program. Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2025	C	`conf`	An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. FORTE Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2024	B	`conf`	Typed Compositional Quantum Computation with Lenses. ITP Jacques Garrigue, Takafumi Saikawa
2023	J	`jnl`	A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory. CoRR Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2023	J	`jnl`	An intuitionistic set-theoretical model of fully dependent CC. Math. Struct. Comput. Sci. Masahiro Sato, Jacques Garrigue
2023	J	`jnl`	Typed compositional quantum computation with lenses. CoRR Jacques Garrigue, Takafumi Saikawa
2021	J	`jnl`	A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
2020	J	`jnl`	A Library for Formalization of Linear Error-Correcting Codes. J. Autom. Reason. Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020	J	`jnl`	A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism. CoRR Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
2020	J	`jnl`	An Intuitionistic Set-theoretical Model of Fully Dependent CCω. CoRR Masahiro Sato, Jacques Garrigue
2020	C	`conf`	Formal Adventures in Convex and Conical Spaces. CICM Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020	J	`jnl`	Formal Adventures in Convex and Conical Spaces. CoRR Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2019	J	`jnl`	Lightweight Linearly-typed Programming with Lenses and Monads. J. Inf. Process. Keigo Imai, Jacques Garrigue
2019	B	`conf`	Proving Tree Algorithms for Succinct Data Structures. ITP Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka
2019	J	`jnl`	Proving tree algorithms for succinct data structures. CoRR Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka
2018	C	`conf`	Examples of Formal Proofs about Data Compression. ISITA Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2018	J	`jnl`	Safe Low-level Code Generation in Coq Using Monomorphization and Monadification. J. Inf. Process. Akira Tanaka, Reynald Affeldt, Jacques Garrigue
2016	J	`jnl`	An Intuitionistic Set-theoretical Model of CC J. Inf. Process. Masahiro Sato, Jacques Garrigue
2016	C	`conf`	Formal Verification of the rank Algorithm for Succinct Data Structures. ICFEM Akira Tanaka, Reynald Affeldt, Jacques Garrigue
2016	C	`conf`	Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. ISITA Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2016	A	`ed.`	Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 ICFP Jacques Garrigue, Gabriele Keller, Eijiro Sumii
2015	J	`jnl`	A certified implementation of ML with structural polymorphism and recursive types. Math. Struct. Comput. Sci. Jacques Garrigue
2015	B	`conf`	Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. ITP Reynald Affeldt, Jacques Garrigue
2015	—	`conf`	GADTs and Exhaustiveness: Looking for the Impossible. ML Family/OCaml Jacques Garrigue, Jacques Le Normand
2015	—	`ed.`	Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014. ML/OCaml Oleg Kiselyov, Jacques Garrigue
2014	B	`ed.`	Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings APLAS Jacques Garrigue
2014	J	`jnl`	Summer School on Coq (NII Shonan Meeting 2014-9). NII Shonan Meet. Rep. Pierre Castéran, Jacques Garrigue, David Nowak
2013	B	`conf`	Ambivalent Types for Principal Type Inference with GADTs. APLAS Jacques Garrigue, Didier Rémy
2011	A	`conf`	A syntactic type system for recursive modules. OOPSLA Hyeonseung Im, Keiko Nakata, Jacques Garrigue, Sungwoo Park
2011	J	`jnl`	Path resolution for nested recursive modules. High. Order Symb. Comput. Jacques Garrigue, Keiko Nakata
2010	B	`conf`	A Certified Implementation of ML with Structural Polymorphism. APLAS Jacques Garrigue
2008	Misc	`ed.`	Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings FLOPS Jacques Garrigue, Manuel V. Hermenegildo
2006	B	`conf`	Private Row Types: Abstracting the Unnamed. APLAS Jacques Garrigue
2006	A	`conf`	Recursive modules for programming. ICFP Keiko Nakata, Jacques Garrigue
2005	—	`conf`	SOBA Framework: An Application Framework for Broadband Network Environment. SAINT Nobuaki Yoshida, Yoshio Hayashi, Yutaka Tamagaki, Shoji Urashita, Makoto Kakuta, Masahiro Watanabe, Jacques Garrigue, Reiji Nakajima
2004	Misc	`conf`	Relaxing the Value Restriction. FLOPS Jacques Garrigue
2002	B	`conf`	Relaxing the Value Restriction. APLAS Jacques Garrigue
2001	B	`conf`	Simple Type Inference for Structural Polymorphism. APLAS Jacques Garrigue
1999	J	`jnl`	Semi-Explicit First-Class Polymorphism for ML. Inf. Comput. Jacques Garrigue, Didier Rémy
1998	A	`conf`	On the Runtime Complexity of Type-Directed Unboxing. ICFP Yasuhiko Minamide, Jacques Garrigue
1997	—	`conf`	Extending ML with Semi-Explicit Higher-Order Polymorphism. TACS Jacques Garrigue, Didier Rémy
1995	J	`jnl`	Label-Selective lambda-Calculus Syntax and Confluence. Theor. Comput. Sci. Hassan Aït-Kaci, Jacques Garrigue
1995	—	`conf`	The Transformation Calculus. FSTTCS Jacques Garrigue
1994	A*	`conf`	The Typed Polymorphic Label-Selective lambda-Calculus. POPL Jacques Garrigue, Hassan Aït-Kaci
1993	—	`conf`	Label-Selective lambda-Calculus Syntax and Confluence. FSTTCS Hassan Aït-Kaci, Jacques Garrigue