Merge branch 'master' of github.com:jcailler/jcailler.github.io

Author: jcailler

_posts/2025-07-29-CADE25.md

@@ -9,5 +9,5 @@ math: true
 mermaid: true
 attachment: cade30.pdf
 bibtex: cade30.txt
-doi: 
+doi: https://dl.acm.org/doi/10.1007/978-3-031-99984-0_18
 ---

_posts/2025-10-31-talk-veridis-retreat.md

@@ -0,0 +1,10 @@
+---
+title: "Deskolemization: From Tableaux to Machine-Checkable Proofs"
+subtitle: VeriDis team seminar, Loria, France
+author:
+date: 2025-10-31
+categories: [talks]
+math: true
+mermaid: true
+attachment: epn_symposium.pdf
+---

_tabs/activities.md

@@ -24,6 +24,7 @@ Together with [Simon Guilloud](https://simonguilloud.ch/), we organize the [Proo
 * International Symposium on Theoretical Aspects of Software Engineering --- **TASE** ([2025](https://cyprusconferences.org/tase2025/))
 
 ## Journal Reviewer
+* [Science of Computer Programming](https://www.sciencedirect.com/journal/science-of-computer-programming)
 * [Journal of Logical and Algebraic Methods in Programming](https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming)
 * [Journal of Applied Logic](https://www.collegepublications.co.uk/ifcolog/)
 

_tabs/tools.md

@@ -55,14 +55,20 @@ SC-TPTP Utilities is a library of tools able to deal with the SC-TPTP format. It
 
 <div>
 <pre>
-@inproceedings{guilloud2025interoperability,
-  title={Interoperability of Proof Systems with SC-TPTP},
-  author={Guilloud, Simon and Cailler, Julie and Gambhir, Sankalp and Poiroux, Auguste and Herklotz, Yann and Bourgeat, Thomas and Kun{\v{c}}ak, Viktor},
-  booktitle={Automated Deduction--CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings},
-  volume={15943},
-  pages={325},
-  year={2025},
-  organization={Springer Nature}
+@inproceedings{10.1007/978-3-031-99984-0_18,
+author = {Guilloud, Simon and Cailler, Julie and Gambhir, Sankalp and Poiroux, Auguste and Herklotz, Yann and Bourgeat, Thomas and Kun\v{c}ak, Viktor},
+title = {Interoperability of&nbsp;Proof Systems with&nbsp;SC-TPTP},
+year = {2025},
+isbn = {978-3-031-99983-3},
+publisher = {Springer-Verlag},
+address = {Berlin, Heidelberg},
+url = {https://doi.org/10.1007/978-3-031-99984-0_18},
+doi = {10.1007/978-3-031-99984-0_18},
+abstract = {We introduce SC-TPTP, an extension of the TPTP derivation format that supports sequent formalism, enabling seamless proof exchange between interactive theorem provers and first-order automated theorem provers. We provide a way to represent non-deductive steps—Skolemization, clausification, and Tseitin normal form—as deductive steps within the format. Building upon the existing support in the Lisa proof assistant and the Go\'{e}land theorem prover, SC-TPTP ecosystem is further enhanced with proof output interfaces for Egg and Prover9, as well as proof reconstruction support for HOL Light, Lean, and Rocq.},
+booktitle = {Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings},
+pages = {325–340},
+numpages = {16},
+location = {Stuttgart, Germany}
 }
 </pre>
 </div>

assets/bibtex/cade30.txt

@@ -1,9 +1,15 @@
-@inproceedings{guilloud2025interoperability,
-  title={Interoperability of Proof Systems with SC-TPTP},
-  author={Guilloud, Simon and Cailler, Julie and Gambhir, Sankalp and Poiroux, Auguste and Herklotz, Yann and Bourgeat, Thomas and Kun{\v{c}}ak, Viktor},
-  booktitle={Automated Deduction--CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings},
-  volume={15943},
-  pages={325},
-  year={2025},
-  organization={Springer Nature}
+@inproceedings{10.1007/978-3-031-99984-0_18,
+author = {Guilloud, Simon and Cailler, Julie and Gambhir, Sankalp and Poiroux, Auguste and Herklotz, Yann and Bourgeat, Thomas and Kun\v{c}ak, Viktor},
+title = {Interoperability of Proof Systems with SC-TPTP},
+year = {2025},
+isbn = {978-3-031-99983-3},
+publisher = {Springer-Verlag},
+address = {Berlin, Heidelberg},
+url = {https://doi.org/10.1007/978-3-031-99984-0_18},
+doi = {10.1007/978-3-031-99984-0_18},
+abstract = {We introduce SC-TPTP, an extension of the TPTP derivation format that supports sequent formalism, enabling seamless proof exchange between interactive theorem provers and first-order automated theorem provers. We provide a way to represent non-deductive steps—Skolemization, clausification, and Tseitin normal form—as deductive steps within the format. Building upon the existing support in the Lisa proof assistant and the Go\'{e}land theorem prover, SC-TPTP ecosystem is further enhanced with proof output interfaces for Egg and Prover9, as well as proof reconstruction support for HOL Light, Lean, and Rocq.},
+booktitle = {Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings},
+pages = {325–340},
+numpages = {16},
+location = {Stuttgart, Germany}
 }