Document Open Access Logo

Open Higher-Order Logic

Authors Ugo Dal Lago , Francesco Gavazzo , Alexis Ghyselen

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.17.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • Department of Computer Science and Engineering, University of Bologna, Italy
Francesco Gavazzo
  • Department of Computer Science, University of Pisa, Italy
Alexis Ghyselen
  • Department of Computer Science and Engineering, University of Bologna, Italy

Funding

This work was funded by the ERC CoG "DIAPASoN" GA 818616.

Cite AsGet BibTex

Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen. Open Higher-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.17

Abstract

We introduce a variation on Barthe et al.’s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function’s domain of definition.

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
  • Theory of computation → Logic and verification
Keywords
  • Formal Verification
  • Relational Logic
  • First-Order Properties

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak, Marco Gaboardi, and Deepak Garg. Relational reasoning for markov chains in a probabilistic guarded lambda calculus. In Proc. of ESOP 2018, volume 10801 of LNCS, pages 214-241. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_8.
  2. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. A relational logic for higher-order programs. Proc. ACM Program. Lang., 1(ICFP):21:1-21:29, 2017. URL: https://doi.org/10.1145/3110265.
  3. Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo. On the versatility of open logical relations: Continuity, automatic differentiation, and a containment theorem. In Proc. of ESOP 2020, volume 12075 of LNCS. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_3.
  4. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  5. Stephen A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70-90, 1978. URL: https://doi.org/10.1137/0207005.
  6. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for lambda-terms. Archiv fur mathematische Logik und Grundlagenforschung, 19(1):139-156, 1978. URL: https://doi.org/10.1007/BF02011875.
  7. Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. In Proc. of LICS 2011, pages 133-142, 2011. URL: https://doi.org/10.1109/LICS.2011.22.
  8. Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen. Open higher-order logic (long version), 2022. URL: http://arxiv.org/abs/2211.06671.
  9. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Proc. of ICFP 2000, pages 198-208, 2000. URL: https://doi.org/10.1145/351240.351259.
  10. Robert W Floyd. Assigning meanings to programs. In Program Verification, pages 65-81. Springer, 1993. Google Scholar
  11. Alejandro Aguirre Galindo. Relational Logics for Higher-Order Effectful Programs. Ph.D Thesis, 2020. Google Scholar
  12. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  13. Martin Hofmann. Linear types and non-size-increasing polynomial time computation. Information and Computation, 183(1):57-85, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00009-9.
  14. Mathieu Huot, Sam Staton, and Matthijs Vákár. Correctness of automatic differentiation via diffeologies and categorical gluing. In Proc. of FoSSACS 2020, volume 12077 of LNCS, pages 319-338. Springer, 2020. Google Scholar
  15. Achim Jung and Jerzy Tiuryn. A new characterization of lambda definability. In Proc. of TLCA 1993, volume 664 of LNCS, pages 245-257. Springer, 1993. URL: https://doi.org/10.1007/BFb0037110.
  16. Damiano Mazza and Michele Pagani. Automatic differentiation in PCF. Proc. ACM Program. Lang., 5(POPL):1-27, 2021. URL: https://doi.org/10.1145/3434309.
  17. Gordon Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM-4, University of Edinburgh, 1973. Google Scholar
  18. Francois Pottier. A simple view of type-secure information flow in the pi-calculus. In Proc. of CSFW 2002, pages 320-330, 2002. URL: https://doi.org/10.1109/CSFW.2002.1021826.
  19. Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu. Formal verification of higher-order probabilistic programs: Reasoning about approximation, convergence, bayesian inference, and optimization. Proc. ACM Program. Lang., 3(POPL):38:1-38:30, 2019. URL: https://doi.org/10.1145/3290351.
  20. Amir Shaikhha, Andrew Fitzgibbon, Dimitrios Vytiniotis, and Simon Peyton Jones. Efficient differentiable programming in a functional array-processing language. Proc. ACM Program. Lang., 3(ICFP):97:1-97:30, 2019. URL: https://doi.org/10.1145/3341701.
  21. Richard Statman. Logical relations and the typed lambda-calculus. Information and Control, 65(2):85-97, 1985. URL: https://doi.org/10.1016/S0019-9958(85)80001-2.
  22. Sam Staton, Frank Wood, Hongseok Yang, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proc. of LICS 2016, pages 525-534, 2016. URL: https://doi.org/10.1145/2933575.2935313.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact