Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Nathan Mull. An Irrelevancy-Eliminating Translation of Pure Type Systems. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 7:1-7:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{mull:LIPIcs.TYPES.2022.7, author = {Mull, Nathan}, title = {{An Irrelevancy-Eliminating Translation of Pure Type Systems}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {7:1--7:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.7}, URN = {urn:nbn:de:0030-drops-184501}, doi = {10.4230/LIPIcs.TYPES.2022.7}, annote = {Keywords: pure type systems, normalization, reduction-path-preserving translations, Barendregt-Geuvers-Klop conjecture} }
Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)
Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk). In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 3:1-3:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2022.3, author = {Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre}, title = {{The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs}}, booktitle = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)}, pages = {3:1--3:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-261-7}, ISSN = {1868-8969}, year = {2022}, volume = {250}, editor = {Dawar, Anuj and Guruswami, Venkatesan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.3}, URN = {urn:nbn:de:0030-drops-173957}, doi = {10.4230/LIPIcs.FSTTCS.2022.3}, annote = {Keywords: two-player games on graphs, finite-memory strategies, chromatic memory, parity automata, \omega-regularity} }
Published in: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus (Artifact). In Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 1, pp. 3:1-3:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@Article{roux_et_al:DARTS.8.1.3, author = {Roux, Pierre and Quinton, Sophie and Boyer, Marc}, title = {{A Formal Link Between Response Time Analysis and Network Calculus (Artifact)}}, pages = {3:1--3:3}, journal = {Dagstuhl Artifacts Series}, ISSN = {2509-8195}, year = {2022}, volume = {8}, number = {1}, editor = {Roux, Pierre and Quinton, Sophie and Boyer, Marc}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.1.3}, URN = {urn:nbn:de:0030-drops-164990}, doi = {10.4230/DARTS.8.1.3}, annote = {Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq} }
Published in: LIPIcs, Volume 231, 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 5:1-5:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{roux_et_al:LIPIcs.ECRTS.2022.5, author = {Roux, Pierre and Quinton, Sophie and Boyer, Marc}, title = {{A Formal Link Between Response Time Analysis and Network Calculus}}, booktitle = {34th Euromicro Conference on Real-Time Systems (ECRTS 2022)}, pages = {5:1--5:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-239-6}, ISSN = {1868-8969}, year = {2022}, volume = {231}, editor = {Maggio, Martina}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2022.5}, URN = {urn:nbn:de:0030-drops-163224}, doi = {10.4230/LIPIcs.ECRTS.2022.5}, annote = {Keywords: Response Time Analysis, Network Calculus, dense time, discrete time, response time, formal proof, Coq} }
Published in: LIPIcs, Volume 231, 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Marco Maida, Sergey Bozhko, and Björn B. Brandenburg. Foundational Response-Time Analysis as Explainable Evidence of Timeliness. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 19:1-19:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{maida_et_al:LIPIcs.ECRTS.2022.19, author = {Maida, Marco and Bozhko, Sergey and Brandenburg, Bj\"{o}rn B.}, title = {{Foundational Response-Time Analysis as Explainable Evidence of Timeliness}}, booktitle = {34th Euromicro Conference on Real-Time Systems (ECRTS 2022)}, pages = {19:1--19:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-239-6}, ISSN = {1868-8969}, year = {2022}, volume = {231}, editor = {Maggio, Martina}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2022.19}, URN = {urn:nbn:de:0030-drops-163363}, doi = {10.4230/LIPIcs.ECRTS.2022.19}, annote = {Keywords: hard real-time systems, response-time analysis, uniprocessor, Coq, Prosa, fixed priority, EDF, preemptive, non-preemptive, verification} }
Published in: DARTS, Volume 7, Issue 1, Special Issue of the 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)
Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact). In Special Issue of the 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 1, pp. 2:1-2:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@Article{boyer_et_al:DARTS.7.1.2, author = {Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David}, title = {{A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus (Artifact)}}, pages = {2:1--2:3}, journal = {Dagstuhl Artifacts Series}, ISSN = {2509-8195}, year = {2021}, volume = {7}, number = {1}, editor = {Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.1.2}, URN = {urn:nbn:de:0030-drops-139810}, doi = {10.4230/DARTS.7.1.2}, annote = {Keywords: Network Calculus, response time, residual curve, rate-latency server, sporadic workload, formal proof, Coq} }
Published in: LIPIcs, Volume 196, 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)
Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus. In 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 196, pp. 14:1-14:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{boyer_et_al:LIPIcs.ECRTS.2021.14, author = {Boyer, Marc and Roux, Pierre and Daigmorte, Hugo and Puechmaille, David}, title = {{A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus}}, booktitle = {33rd Euromicro Conference on Real-Time Systems (ECRTS 2021)}, pages = {14:1--14:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-192-4}, ISSN = {1868-8969}, year = {2021}, volume = {196}, editor = {Brandenburg, Bj\"{o}rn B.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2021.14}, URN = {urn:nbn:de:0030-drops-139457}, doi = {10.4230/LIPIcs.ECRTS.2021.14}, annote = {Keywords: Network Calculus, response time, residual curve, rate-latency server, sporadic workload, formal proof, Coq} }
Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)
Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games Where You Can Play Optimally with Arena-Independent Finite Memory. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 24:1-24:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2020.24, author = {Bouyer, Patricia and Le Roux, St\'{e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, title = {{Games Where You Can Play Optimally with Arena-Independent Finite Memory}}, booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)}, pages = {24:1--24:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-160-3}, ISSN = {1868-8969}, year = {2020}, volume = {171}, editor = {Konnov, Igor and Kov\'{a}cs, Laura}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.24}, URN = {urn:nbn:de:0030-drops-128360}, doi = {10.4230/LIPIcs.CONCUR.2020.24}, annote = {Keywords: two-player games on graphs, finite-memory determinacy, optimal strategies} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux. A Verified LL(1) Parser Generator. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lasser_et_al:LIPIcs.ITP.2019.24, author = {Lasser, Sam and Casinghino, Chris and Fisher, Kathleen and Roux, Cody}, title = {{A Verified LL(1) Parser Generator}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {24:1--24:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.24}, URN = {urn:nbn:de:0030-drops-110794}, doi = {10.4230/LIPIcs.ITP.2019.24}, annote = {Keywords: interactive theorem proving, top-down parsing} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{bertholon_et_al:LIPIcs.ITP.2019.7, author = {Bertholon, Guillaume and Martin-Dorel, \'{E}rik and Roux, Pierre}, title = {{Primitive Floats in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {7:1--7:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7}, URN = {urn:nbn:de:0030-drops-110629}, doi = {10.4230/LIPIcs.ITP.2019.7}, annote = {Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition} }
Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)
Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.8, author = {Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael}, title = {{Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.8}, URN = {urn:nbn:de:0030-drops-109103}, doi = {10.4230/LIPIcs.CONCUR.2019.8}, annote = {Keywords: Markov decision processes, window mean-payoff, window parity} }
Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)
Marco Gaboardi and Justin Hsu. A Theory AB Toolbox. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 129-139, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{gaboardi_et_al:LIPIcs.SNAPL.2015.129, author = {Gaboardi, Marco and Hsu, Justin}, title = {{A Theory AB Toolbox}}, booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)}, pages = {129--139}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-80-4}, ISSN = {1868-8969}, year = {2015}, volume = {32}, editor = {Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.129}, URN = {urn:nbn:de:0030-drops-50225}, doi = {10.4230/LIPIcs.SNAPL.2015.129}, annote = {Keywords: Verification, randomized algorithms} }
Feedback for Dagstuhl Publishing