1. Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa. A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism. arXiv:2003.09993 [cs], March 2020. Keyword(s): probability. [Abstract] [bibtex-entry]



2. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. A Library for Formalization of Linear Error-Correcting Codes. Journal of Automated Reasoning, January 2020. ISSN: 1573-0670. Keyword(s): Coq, probability. [Abstract] [bibtex-entry]



3. Davide Ancona, Pietro Barbieri, Francesco Dagnino, and Elena Zucca. Sound Regular Corecursion in coFJ. arXiv:2005.14085 [cs], May 2020. Keyword(s): Java, streams. [Abstract] [bibtex-entry]



4. Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Abstract Interpretation of Distributed Network Control Planes. Proceedings of the ACM on Programming Languages, 4(POPL):1-27, January 2020. ISSN: 2475-1421, 2475-1421. Keyword(s): abstract interpretation. [bibtex-entry]



5. Gianluca Curzi and Luca Roversi. Probabilistic Soft Type Assignment. arXiv:2007.01733 [cs], July 2020. Keyword(s): calculus, probability. [Abstract] [bibtex-entry]

1. B. Lacerda, F. Faruq, D. Parker, and N. Hawes. Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots. International Journal of Robotics Research, 38(19):1098-1123, 2019. Keyword(s): model checking, probability. [bibtex-entry]



2. Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for Verifying Deep Neural Networks. arXiv:1903.06758 [cs, stat], March 2019. Keyword(s): model checking. [Abstract] [bibtex-entry]

1. Gul Agha and Karl Palmskog. A Survey of Statistical Model Checking. ACM Transactions on Modeling and Computer Simulation, 28(1):6:1-6:39, January 2018. ISSN: 1049-3301. Keyword(s): model checking. [Abstract] [bibtex-entry]



2. Laura Titolo, Marco A. Feliú, Mariano Moscato, and César A. Muñoz. An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation, volume 10747, pages 516-537. Springer International Publishing, Cham, 2018. ISBN: 978-3-319-73720-1 978-3-319-73721-8. Keyword(s): abstract interpretation. [Abstract] [bibtex-entry]

1. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A Formally Verified Proof of the Central Limit Theorem. Journal of Automated Reasoning, 59(4):389-423, December 2017. ISSN: 1573-0670. Keyword(s): HOL, Isabelle, probability. [Abstract] [bibtex-entry]



2. Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science, 12(3):7, April 2017. ISSN: 18605974. Keyword(s): calculus, streams. [Abstract] [bibtex-entry]

1. Matthew Chan, Daniel Ricketts, Sorin Lerner, and Gregory Malecha. Formal Verification of Stability Properties of Cyber-Physical Systems. pp 2, 2016. Keyword(s): Coq, verification. [bibtex-entry]



2. Robert Kelly, Barak A. Pearlmutter, and Jeffrey Mark Siskind. Evolving the Incremental Lambda Calculus into a Model of Forward Automatic Differentiation (AD). arXiv:1611.03429 [cs], November 2016. Keyword(s): calculus. [Abstract] [bibtex-entry]



3. Stefan Mitsch and André Platzer. ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. Formal Methods in System Design, 49(1):33-74, October 2016. ISSN: 1572-8102. Keyword(s): verification. [Abstract] [bibtex-entry]

1. Stefan Milius and Thorsten Wissmann. Finitary Corecursion for the Infinitary Lambda Calculus. arXiv:1505.07736 [cs, math], May 2015. Keyword(s): calculus, coinduction, Haskell. [Abstract] [bibtex-entry]



2. Abhishek Anand and Ross Knepper. ROSCoq: Robots Powered by Constructive Reals. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, volume 9236, pages 34-50. Springer International Publishing, Cham, 2015. ISBN: 978-3-319-22101-4 978-3-319-22102-1. Keyword(s): Coq, reals, verification. [Abstract] [bibtex-entry]

1. Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell. Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. Journal of Aerospace Information Systems, 11(10):702-713, 2014. Keyword(s): avionics, verification. [Abstract] [bibtex-entry]



2. Conor Thomas McBride. How to Keep Your Neighbours in Order. ACM SIGPLAN Notices, 49(9):297-309, November 2014. ISSN: 0362-1340, 1558-1160. Keyword(s): Agda. [bibtex-entry]



3. Tobias Nipkow and Gerwin Klein. Abstract Interpretation. In Tobias Nipkow and Gerwin Klein, editors, Concrete Semantics: With Isabelle/HOL, pages 219-280. Springer International Publishing, Cham, 2014. ISBN: 978-3-319-10542-0. Keyword(s): abstract interpretation. [Abstract] [bibtex-entry]

1. Liya Liu, Osman Hasan, and Sofiène Tahar. Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL. Journal of Computer Science and Technology, 28(2):217-231, March 2013. ISSN: 1860-4749. Keyword(s): probability, verification. [Abstract] [bibtex-entry]



2. Lee Pike, Nis Wegmann, Sebastian Niller, and Alwyn Goodloe. Copilot: Monitoring Embedded Systems. Innovations in Systems and Software Engineering, 9(4):235-255, December 2013. ISSN: 1614-5046, 1614-5054. Keyword(s): Haskell, streams, verification. [bibtex-entry]

1. Vibhav Gogate and Pedro Domingos. Probabilistic Theorem Proving. arXiv:1202.3724 [cs], February 2012. Keyword(s): probability. [Abstract] [bibtex-entry]



2. Ugo Dal Lago and Margherita Zorzi. Probabilistic Operational Semantics for the Lambda Calculus. RAIRO - Theoretical Informatics and Applications, 46(3):413-450, July 2012. ISSN: 0988-3754, 1290-385X. Keyword(s): calculus, probability. [Abstract] [bibtex-entry]



3. Diogo Araújo Carvalho Vilaça Moreira. Finite Probability Distributions in Coq. April 2012. Keyword(s): Coq, probability. [Abstract] [bibtex-entry]



4. Paula G. Severi and Fer-Jan J. de Vries. Pure Type Systems with Corecursion on Streams: From Finite to Infinitary Normalisation. ACM SIGPLAN Notices, 47(9):141-152, September 2012. ISSN: 0362-1340. Keyword(s): calculus, coinduction. [Abstract] [bibtex-entry]

1. Sergey Goncharov and Lutz Schröder. A Coinductive Calculus for Asynchronous Side-Effecting Processes. arXiv:1104.2936 [cs], April 2011. Keyword(s): asynchronous, calculus. [Abstract] [bibtex-entry]



2. Osman Hasan and Sofiène Tahar. Reasoning about Conditional Probabilities in a Higher-Order-Logic Theorem Prover. Journal of Applied Logic, 9(1):23-40, March 2011. ISSN: 1570-8683. Keyword(s): HOL, probability. [Abstract] [bibtex-entry]



3. Ugo Dal Lago and Margherita Zorzi. Probabilistic Operational Semantics for the Lambda Calculus. arXiv:1104.0195 [cs], June 2011. Keyword(s): calculus, probability. [Abstract] [bibtex-entry]



4. Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, and David Parker. Automated Verification Techniques for Probabilistic Systems. In Marco Bernardo and Valérie Issarny, editors, Formal Methods for Eternal Networked Software Systems, volume 6659, pages 53-113. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. ISBN: 978-3-642-21454-7 978-3-642-21455-4. Keyword(s): probability, verification. [Abstract] [bibtex-entry]

1. Ralf Hinze. Concrete Stream Calculus: An Extended Study. Journal of Functional Programming, 20(5-6):463-535, November 2010. ISSN: 0956-7968, 1469-7653. Keyword(s): coinduction, Haskell. [Abstract] [bibtex-entry]



2. Taylor. A Lambda Calculus for Real Analysis. Journal of Logic and Analysis, 2010. ISSN: 17599008. Keyword(s): calculus, reals. [Abstract] [bibtex-entry]

1. Osman Hasan and Sofiène Tahar. Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical Methods in the Applied Sciences, 32(4):480-504, March 2009. ISSN: 01704214, 10991476. Keyword(s): HOL, probability. [Abstract] [bibtex-entry]



2. Osman Hasan and Sofiène Tahar. Probabilistic Analysis of Wireless Systems Using Theorem Proving. Electronic Notes in Theoretical Computer Science, 242(2):43-58, July 2009. ISSN: 15710661. Keyword(s): HOL, probability. [Abstract] [bibtex-entry]



3. Favio Ezequiel Miranda-Perea. Two Extensions of System F with (Co)Iteration and Primitive (Co)Recursion Principles. RAIRO - Theoretical Informatics and Applications, 43(4):703-766, October 2009. ISSN: 0988-3754, 1290-385X. Keyword(s): calculus, coinduction. [Abstract] [bibtex-entry]

1. Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective Typestate Verification in the Presence of Aliasing. ACM Transactions on Software Engineering and Methodology, 17(2):1-34, April 2008. ISSN: 1049-331X, 1557-7392. Keyword(s): abstract interpretation. [bibtex-entry]



2. Osman Hasan and Sofiène Tahar. Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, 41(3-4):295-323, November 2008. ISSN: 0168-7433, 1573-0670. Keyword(s): HOL, probability. [Abstract] [bibtex-entry]



3. André Platzer. Differential Dynamic Logic for Hybrid Systems. Journal of Automated Reasoning, 41(2):143-189, August 2008. ISSN: 1573-0670. Keyword(s): verification. [Abstract] [bibtex-entry]



4. J. J. M. M. Rutten. Rational Streams Coalgebraically. Logical Methods in Computer Science, 4(3):9, September 2008. ISSN: 18605974. Keyword(s): streams. [Abstract] [bibtex-entry]

1. Yannick Moy and Claude Marché. Inferring Local (Non-) Aliasing and Strings for Memory Safety. Heap Analysis and Verification (HAV'07), pp 35-51, 2007. Keyword(s): abstract interpretation. [bibtex-entry]



2. Sumit Gulwani and Ashish Tiwari. An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, volume 4590, pages 379-392. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. ISBN: 978-3-540-73367-6. Keyword(s): abstract interpretation. [bibtex-entry]



3. Osman Hasan and Sofiène Tahar. Formalization of Continuous Probability Distributions. In Frank Pfenning, editor, Automated Deduction - CADE-21, volume 4603, pages 3-18. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. ISBN: 978-3-540-73594-6 978-3-540-73595-3. ISSN: 0302-9743, 1611-3349. Keyword(s): HOL, probability. [Abstract] [bibtex-entry]

1. Gul Agha, José Meseguer, and Koushik Sen. PMaude: Rewrite-Based Specification Language for Probabilistic Object Systems. Electronic Notes in Theoretical Computer Science, 153(2):213-239, May 2006. ISSN: 1571-0661. Keyword(s): actors, asynchronous, probability. [Abstract] [bibtex-entry]



2. Alberto Ciaffaglione and Pietro Di Gianantonio. A Certified, Corecursive Implementation of Exact Real Numbers. Theoretical Computer Science, 351(1):39-51, February 2006. ISSN: 0304-3975. Keyword(s): Coq, reals. [Abstract] [bibtex-entry]



3. Antoine Miné. The Octagon Abstract Domain. Higher-Order and Symbolic Computation, 19(1):31-100, March 2006. ISSN: 1573-0557. Keyword(s): abstract interpretation. [Abstract] [bibtex-entry]



4. Peter Selinger and Benoit Valiron. A Lambda Calculus for Quantum Computation with Classical Control. Mathematical Structures in Computer Science, 16(3):527-552, June 2006. ISSN: 0960-1295. Keyword(s): calculus, quantum. [Abstract] [bibtex-entry]



5. Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In Holger Hermanns and Jens Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 3920, pages 441-444. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. ISBN: 978-3-540-33056-1 978-3-540-33057-8. Keyword(s): model checking, probability. [Abstract] [bibtex-entry]

1. Wilfried Buchholz. A Term Calculus for (Co-)Recursive Definitions on Streamlike Data Structures. Annals of Pure and Applied Logic, 136(1):75-90, October 2005. ISSN: 0168-0072. Keyword(s): calculus, streams. [Abstract] [bibtex-entry]



2. Koushik Sen, Mahesh Viswanathan, and Gul Agha. On Statistical Model Checking of Stochastic Systems. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Dough Tygar, Moshe Y. Vardi, Gerhard Weikum, Kousha Etessami, and Sriram K. Rajamani, editors, Computer Aided Verification, volume 3576, pages 266-280. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005. ISBN: 978-3-540-27231-1 978-3-540-31686-2. Keyword(s): model checking, probability. [Abstract] [bibtex-entry]

1. Thomas Ehrhard and Laurent Regnier. The Differential Lambda-Calculus. Theoretical Computer Science, 309(1):1-41, December 2003. ISSN: 0304-3975. Keyword(s): calculus. [Abstract] [bibtex-entry]

1. J. J. M. M. Rutten. Elements of Stream Calculus: (An Extensive Exercise in Coinduction). Electronic Notes in Theoretical Computer Science, 45:358-423, November 2001. ISSN: 1571-0661. Keyword(s): reals, streams. [Abstract] [bibtex-entry]

1. Lawrence C. Paulson. Mechanizing Coinduction and Corecursion in Higher-Order Logic. Journal of Logic and Computation, 7(2):175-204, April 1997. ISSN: 0955-792X. Keyword(s): coinduction, HOL. [Abstract] [bibtex-entry]

1. Arnaud Venet. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Radhia Cousot, and David A. Schmidt, editors, Static Analysis, volume 1145, pages 366-382. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. ISBN: 978-3-540-61739-6 978-3-540-70674-8. Keyword(s): abstract interpretation. [bibtex-entry]

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.

This document was translated from BibT_EX by bibtex2html