@inproceedings{saito2023aplas,
author = {Reynald Affeldt and Ayumu Saito},
title = {Experimenting with an Intrinsically-typed Probabilistic Programming Language in {Coq}},
booktitle = {21st Asian Symposium on Programming Languages and Systems (\href{https://conf.researchr.org/home/aplas-2023}{APLAS 2023}), Taipei, Taiwan, November 26--29, 2023},
year = {2023},
editor = {},
volume = {14405},
number = {},
series = {},
pages = {182-202},
address = {},
month = {Nov},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-981-99-8311-7_9}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/syntax-aplas2023.pdf}{pdf preprint}}
}
@inproceedings{affeldt2023cpp,
author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito},
title = {Semantics of Probabilistic Programs using s-Finite Kernels in {Coq}},
booktitle = {12th ACM SIGPLAN Conference on Certified Programs and Proofs (\href{https://popl23.sigplan.org/home/CPP-2023}{CPP 2023}), Boston, MA, USA, January 16--17, 2023},
year = {2023},
editor = {},
volume = {},
number = {},
series = {},
pages = {3-16},
address = {},
month = {Jan},
organization = {},
publisher = {ACM Press},
abstract = {\href{http://dx.doi.org/10.1145/3573105.3575691}{doi} \href{https://hal.inria.fr/hal-03917948/}{open access}}
}
@inproceedings{saito2022mpc,
author = {Ayumu Saito and Reynald Affeldt},
title = {Towards a Practical Library for Monadic Equational Reasoning in {Coq}},
booktitle = {14th International Conference on Mathematics of Program Construction (\href{https://www.macs.hw.ac.uk/mpc22/}{MPC 2022}), Tbilisi, Georgia, September 26--28, 2022},
year = {2022},
editor = {},
volume = {13544},
number = {},
series = {Lecture Notes in Computer Science},
pages = {151--177},
address = {},
month = {Sep},
organization = {},
publisher = {Springer},
abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/monae-mpc2022.pdf}{pdf preprint} \href{http://dx.doi.org/10.1007/978-3-031-16912-0_6}{doi} \href{https://github.com/affeldt-aist/monae}{project page}}
}
@inproceedings{affeldt2020types,
author = {Reynald Affeldt and David Nowak},
title = {Extending Equational Monadic Reasoning with Monad Transformers},
booktitle = {26th International Conference on Types for Proofs and Programs (\href{https://types2020.di.unito.it/}{TYPES 2020})},
year = {2021},
editor = {},
volume = {188},
number = {},
series = {Leibniz International Proceedings in Informatics},
pages = {2:1--2:21},
address = {},
month = {Jun},
organization = {},
publisher = {Schloss Dagstuhl},
abstract = {\href{http://dx.doi.org/10.4230/LIPIcs.TYPES.2020.2}{doi} Post-Proceedings. arXiv preprint \href{https://arxiv.org/abs/2011.03463}{cs.LO 2011.03463}}
}
@inproceedings{affeldt2020cicm,
author = {Reynald Affeldt and Jacques Garrigue and Takafumi Saikawa},
title = {Formal Adventures in Convex and Conical Spaces},
booktitle = {13th Conference on Intelligent Computer Mathematics (\href{https://cicm-conference.org/2020/}{CICM 2020}), Bertinoro, Forli, Italy, July 26--31, 2020},
year = {2020},
editor = {},
volume = {12236},
number = {},
series = {Lecture Notes in Artificial Intelligence},
pages = {23--38},
address = {},
month = {Jul},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-030-53518-6_2}{doi} \href{https://arxiv.org/abs/2004.12713}{open access}}
}
@inproceedings{affeldt2020ijcar,
author = {Reynald Affeldt and Cyril Cohen and Marie Kerjean and Assia Mahboubi and Damien Rouhling and Kazuhiko Sakaguchi},
title = {Competing inheritance paths in dependent type theory: a case study in functional analysis},
booktitle = {10th International Joint Conference on Automated Reasoning (\href{https://ijcar2020.org/}{IJCAR 2020}), Paris, France, June 29--July 6, 2020},
year = {2020},
editor = {},
volume = {12167},
number = {2},
series = {Lecture Notes in Artificial Intelligence},
pages = {3--20},
address = {},
month = {Jul},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-030-51054-1_1}{doi} \href{https://hal.inria.fr/hal-02463336v2}{open access}}
}
@inproceedings{affeldt2019mpc,
author = {Reynald Affeldt and David Nowak and Takafumi Saikawa},
title = {A Hierarchy of Monadic Effects for Program Verification using Equational Reasoning},
booktitle = {13th International Conference on Mathematics of Program Construction (\href{http://www.cs.nott.ac.uk/~pszgmh/mpc19.html}{MPC 2019}), Porto, Portugal, October 7--9, 2019},
year = {2019},
editor = {},
volume = {11825},
number = {},
series = {Lecture Notes in Computer Science},
pages = {226--254},
address = {},
month = {Oct},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-030-33636-3_9}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf}{pdf preprint} \href{https://github.com/affeldt-aist/monae}{project page}}
}
@inproceedings{affeldt2019itp,
author = {Reynald Affeldt and Jacques Garrigue and Xuanrui Qi and Kazunari Tanaka},
title = {Proving tree algorithms for succinct data structures},
booktitle = {10th International Conference on Interactive Theorem Proving (\href{https://itp19.cecs.pdx.edu/}{ITP 2019}), Portland, OR, USA, September 8-13, 2019},
year = {2019},
editor = {},
volume = {141},
number = {},
series = {Leibniz International Proceedings in Informatics},
pages = {28:1--28:19},
address = {},
month = {Sep},
organization = {},
publisher = {Schloss Dagstuhl},
abstract = {\href{https://doi.org/10.4230/LIPIcs.ITP.2019.5}{open access} \href{http://dx.doi.org/10.4230/LIPIcs.ITP.2019.5}{doi} \href{https://arxiv.org/abs/1904.02809}{pdf preprint} \href{https://github.com/affeldt-aist/succinct}{project page}}
}
@inproceedings{affeldt2018isita,
author = {Reynald Affeldt and Jacques Garrigue and Takafumi Saikawa},
title = {Examples of Formal Proofs about Data Compression},
booktitle = {International Symposium on Information Theory and Its Applications (\href{http://www.isita.ieice.org/2018/home.html}{ISITA 2018}), Singapore, October 28--31, 2018},
year = {2018},
editor = {},
volume = {},
number = {},
series = {},
pages = {633--637},
address = {},
month = {Oct},
organization = {},
publisher = {{IEEE}},
abstract = {\href{http://dx.doi.org/10.23919/ISITA.2018.8664276}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf}{pdf preprint} \href{https://github.com/affeldt-aist/infotheo}{project page}}
}
@inproceedings{affeldt2017cpp,
author = {Reynald Affeldt and Cyril Cohen},
title = {Formal Foundations of {3D} Geometry to Model Robot Manipulators},
booktitle = {6th ACM SIGPLAN Conference on Certified Programs and Proofs (\href{http://cpp2017.mpi-sws.org/}{CPP 2017}), Paris, France, January 16--17, 2017},
year = {2017},
editor = {},
volume = {},
number = {},
series = {},
pages = {30--42},
address = {},
month = {Jan},
organization = {},
publisher = {ACM Press},
abstract = {\href{http://dx.doi.org/10.1145/3018610.3018629}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/robot_cpp_long.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/robot/}{project page} \href{http://staff.aist.go.jp/reynald.affeldt/documents/slides_cpp2017.pdf}{slides}}
}
@inproceedings{tanaka2016icfem,
author = {Akira Tanaka and Reynald Affeldt and Jacques Garrigue},
title = {Formal Verification of the rank Algorithm for Succinct Data Structures},
booktitle = {18th International Conference on Formal Engineering Methods (ICFEM 2016), Tokyo, Japan, November 14--18, 2016},
year = {2016},
editor = {},
volume = {10009},
series = {Lecture Notes in Computer Science},
pages = {243--260},
address = {},
month = {Nov},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-319-47846-3_16}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/succinct-icfem2016-author.pdf}{pdf preprint} \href{https://staff.aist.go.jp/tanaka-akira/succinct/}{project page}}
}
@inproceedings{affeldt2016isita,
author = {Reynald Affeldt and Jacques Garrigue and Takafumi Saikawa},
title = {Formalization of {Reed-Solomon} codes and progress report on formalization of {LDPC} codes},
booktitle = {International Symposium on Information Theory and Its Applications (\href{http://www.isita.ieice.org/2016/index.html}{ISITA 2016}), Monterey, California, USA, October 30--November 2, 2016},
year = {2016},
editor = {},
volume = {},
number = {},
series = {},
pages = {537--541},
address = {},
month = {Oct},
organization = {},
publisher = {IEICE. {IEEE} Xplore},
abstract = {\href{http://dx.doi.org/}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/ecc/}{project page}}
}
@inproceedings{affeldt2015itp,
author = {Reynald Affeldt and Jacques Garrigue},
title = {Formalization of Error-correcting Codes: from {Hamming} to Modern Coding Theory},
booktitle = {6th Conference on Interactive Theorem Proving (\href{https://nms.kcl.ac.uk/christian.urban/itp-2015/}{ITP 2015}), Nanjing, China, August 24--27, 2015},
year = {2015},
editor = {},
volume = {9236},
number = {},
series = {Lecture Notes in Computer Science},
pages = {17--33},
address = {},
month = {Aug},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-319-22102-1_2}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/ecc/}{project page}}
}
@inproceedings{obi2014isita,
author = {Ryosuke Obi and Manabu Hagiwara and Reynald Affeldt},
title = {Formalization of Variable-Length Source Coding Theorem: Direct Part},
booktitle = {International Symposium on Information Theory and Its Applications (ISITA 2014), Melbourne, Australia, October 26--29, 2014},
year = {2014},
editor = {},
volume = {},
number = {},
series = {},
pages = {201--205},
address = {},
month = {Oct},
organization = {},
publisher = {IEICE. IEEE Xplore},
abstract = {}
}
@inproceedings{affeldt2013plpv,
author = {Reynald Affeldt and Nicolas Marti},
title = {Towards Formal Verification of {TLS} Network Packet Processing Written in {C}},
booktitle = {7th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (\href{http://plpv.tcs.ifi.lmu.de/}{PLPV 2013}), Rome, Italy, January 22, 2013},
year = {2013},
editor = {},
volume = {},
number = {},
series = {},
pages = {35--46},
address = {},
month = {Jan},
organization = {},
publisher = {ACM Press},
abstract = {\href{http://dx.doi.org/10.1145/2428116.2428124}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/plpv2013-affeldt-marti.pdf}{pdf preprint}}
}
@inproceedings{affeldt2012itp,
author = {Reynald Affeldt and Manabu Hagiwara},
title = {Formalization of {Shannon}'s Theorems in {SSReflect}-{Coq}},
booktitle = {3rd Conference on Interactive Theorem Proving (\href{http://itp2012.cs.princeton.edu/}{ITP 2012}), Princeton, New Jersey, USA, August 13--15, 2012},
year = {2012},
editor = {},
volume = {7406},
number = {},
series = {Lecture Notes in Computer Science},
pages = {233--249},
address = {},
month = {Aug},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-642-32347-8_16}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-itp2012-preprint.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/shannon/}{project page} \href{http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-itp2012-slides.pdf}{slides}}
}
@inproceedings{affeldt2012sac,
author = {Reynald Affeldt},
title = {On Construction of a Library of Formally Verified Low-level Arithmetic Functions},
booktitle = {27th ACM SIGAPP Symposium On Applied Computing (\href{http://www.sigapp.org/sac/sac2012/}{SAC 2012}), Riva del Garda (Trento), Italy, March 26--30, 2012},
year = {2012},
editor = {},
volume = {2},
number = {},
series = {},
pages = {1326--1331},
address = {},
month = {Mar},
organization = {},
publisher = {ACM Press},
abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/arilib-affeldt.pdf}{pdf preprint} \href{http://dx.doi.org/10.1145/2245276.2231986}{doi} Software Verification and Testing Track \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page}}
}
@inproceedings{nowak2012plpv,
author = {Reynald Affeldt and David Nowak and Yutaka Oiwa},
title = {Formal Network Packet Processing with Minimal Fuss: Invertible Syntax Descriptions at Work},
booktitle = {6th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV 2012), Philadelphia, USA, January 24, 2012},
year = {2012},
editor = {},
volume = {},
number = {},
series = {},
pages = {27--36},
address = {},
month = {Jan},
organization = {},
publisher = {ACM Press},
abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/plpv2012-preprint.pdf}{pdf preprint} \href{http://dx.doi.org/10.1145/2103776.2103781}{doi}}
}
@inproceedings{affeldt2009avocs,
author = {Reynald Affeldt and David Nowak and Kiyoshi Yamada},
title = {Certifying Assembly with Formal Cryptographic Proofs: the Case of {BBS}},
booktitle = {\href{https://journal.ub.tu-berlin.de/eceasst/index}{Electronic Communications of the EASST}},
year = {2010},
editor = {},
volume = {23},
number = {},
series = {},
pages = {},
address = {},
month = {Jan},
organization = {},
publisher = {European Association of Software Science and Technology},
abstract = {\href{http://dx.doi.org/10.14279/tuj.eceasst.23.316}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/certifying_bbs.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/bbs/}{project page} Proceedings of the 9th International Workshop on Automated Verification of Critical Systems (\href{http://www.cs.swan.ac.uk/avocs09/}{AVoCS 2009}), Swansea University Computer Science, September 23--25, 2009. Preliminary version: Technical Report of Computer Science, Swansea University CSR-2-2009}
}
@inproceedings{affeldt2008fcs,
author = {Reynald Affeldt and Hubert Comon-Lundh},
title = {A Note on First-order Logic and Security Protocols},
booktitle = {Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (\href{http://profs.sci.univr.it/~vigano/fcs-arspa-wits08/}{FCS-ARSPA-WITS 2008}), Pittsburgh, PA, USA, June 21--22, 2008},
year = {2008},
editor = {},
volume = {},
number = {},
series = {},
pages = {11--20},
address = {},
month = {Jun},
organization = {},
publisher = {},
abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/fcs2008.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/rigid/}{project page}}
}
@inproceedings{affeldt2007provsec,
author = {Reynald Affeldt and Miki Tanaka and Nicolas Marti},
title = {Formal Proof of Provable Security by Game-playing in a Proof Assistant},
booktitle = {1st International Conference on Provable Security (Provsec 2007), Wollongong, NSW, Australia, November 1--2, 2007},
year = {2007},
editor = {},
volume = {4784},
number = {},
series = {Lecture Notes in Computer Science},
pages = {151--168},
address = {},
month = {Nov},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-540-75670-5_10}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/provsec07.pdf}{pdf preprint}}
}
@inproceedings{affeldt2006asian,
author = {Reynald Affeldt and Nicolas Marti},
title = {An Approach to Formal Verification of Arithmetic Functions in Assembly},
booktitle = {11th Annual Asian Computing Science Conference (ASIAN 2006), Focusing on Secure Software and Related Issues, Tokyo, Japan, December 6--8, 2006},
year = {2008},
editor = {},
volume = {4435},
number = {},
series = {Lecture Notes in Computer Science},
pages = {346--360},
address = {},
month = {Jan},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-540-77505-8_27}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-asian2006.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page}}
}
@inproceedings{marti2006icfem,
author = {Nicolas Marti and Reynald Affeldt and Akinori Yonezawa},
title = {Formal Verification of the Heap Manager of an Operating System using Separation Logic},
booktitle = {8th International Conference on Formal Engineering Methods (ICFEM 2006), Macao SAR, China, October 29--November 3, 2006},
year = {2006},
editor = {},
volume = {4260},
number = {},
series = {Lecture Notes in Computer Science},
pages = {400--419},
address = {},
month = {Oct},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/11901433_22}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/icfem06.pdf}{pdf preprint}}
}
@article{affeldt2004express,
author = {Reynald Affeldt and Naoki Kobayashi},
title = {Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes},
journal = {Electronic Notes in Theoretical Computer Science},
year = {2005},
volume = {128},
number = {2},
pages = {151--168},
month = {Apr},
abstract = {\href{http://dx.doi.org/10.1016/j.entcs.2004.11.034}{doi} Elsevier. Proceedings of the 11th International Workshop on Expressiveness in Concurrency (\href{http://www.win.tue.nl/express04/}{EXPRESS 2004}), London, UK, August 30, 2004 \href{http://staff.aist.go.jp/reynald.affeldt/documents/express04pre.pdf}{pdf preprint} \href{http://staff.aist.go.jp/reynald.affeldt/documents/express04extended.pdf}{pdf preprint}}
}
@article{affeldt2004lfm,
author = {Reynald Affeldt and Naoki Kobayashi},
title = {A {Coq} Library for Verification of Concurrent Programs},
journal = {Electronic Notes in Theoretical Computer Science},
year = {2008},
volume = {199},
number = {},
pages = {17--32},
month = {Feb},
abstract = {\href{http://dx.doi.org/10.1016/j.entcs.2007.11.010}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/lfm04post.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/applpi/}{project page} Elsevier. Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), Cork, Ireland, July 5, 2004}
}
@inproceedings{affeldt2002isse,
author = {Reynald Affeldt and Naoki Kobayashi},
title = {Formalization and Verification of a Mail Server in {Coq}},
booktitle = {International Symposium on Software Security, Tokyo, Japan, November 8--10, 2002},
year = {2003},
editor = {},
volume = {2609},
number = {},
series = {Lecture Notes in Computer Science, Hot Topics},
pages = {217--233},
address = {},
month = {Feb},
organization = {},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/3-540-36532-X_14}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/isss-paper.pdf}{pdf preprint} \href{http://staff.aist.go.jp/reynald.affeldt/documents/isss-slides.pdf}{slides}}
}
@inproceedings{affeldt2002asiapepm,
author = {Reynald Affeldt and Hidehiko Masuhara and Eijiro Sumii and Akinori Yonezawa},
title = {Supporting Objects in Run-Time Bytecode Specialization},
booktitle = {ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-based Program Manipulation (ASIA-PEPM 2002), Aizu, Japan, September 12--14, 2002},
year = {2002},
editor = {},
volume = {},
number = {},
series = {},
pages = {50--60},
address = {},
month = {Sep},
organization = {},
publisher = {ACM Press},
abstract = {\href{http://dx.doi.org/10.1145/568173.568179}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/p50-affeldt.pdf}{pdf preprint} \href{http://staff.aist.go.jp/reynald.affeldt/documents/asia-pepm-slides.pdf}{slides}}
}
This file was generated by bibtex2html 1.99.