相关论文: Proceedings 10th International Workshop on the ACL…

When ACL2 is used to model the operational semantics of computing machines, machine states are typically represented by terms recording the contents of the state components. When models are realistic and are stepped through thousands of…

Neural theorem proving combines large language models (LLMs) with proof assistants such as Lean, where the correctness of formal proofs can be rigorously verified, leaving no room for hallucination. With existing neural theorem provers…

This volume contains the proceedings of DCM 2023, the 13th International Workshop on Developments in Computational Models held on 2 July 2023 in Rome, Italy. DCM 2023 was organised as a one-day satellite event of FSCD 2023, the 8th…

Previous works on formally studying mobile robotic swarms consider necessary and sufficient system hypotheses enabling to solve theoretical benchmark problems (geometric pattern formation, gathering, scattering, etc.). We argue that formal…

Mathematical theorem proving is an important testbed for large language models' deep and abstract reasoning capability. This paper focuses on improving LLMs' ability to write proofs in formal languages that permit automated proof…

Computation nowadays is becoming inherently concurrent, either because of characteristics of the hardware (with multicore processors becoming omnipresent) or due to the ubiquitous presence of distributed systems (incarnated in the…

One important approach to software verification is interactive theorem proving. However, writing formal proofs often requires substantial human effort, making proof automation highly important. Traditionally, proof automation has relied on…

The notion of continuation is ubiquitous in many different areas of computer science, including systems programming, programming languages, algorithmics, semantics, logic, and constructive mathematics. In fact the concept of continuation…

This volume contains a selection of the papers presented at the XVI Jornadas sobre Programaci\'on y Lenguajes (PROLE 2016), held at Salamanca, Spain, during September 14th-15th, 2016. Previous editions of the workshop were held in Santander…

This volume contains the proceedings of the 19th International Conference on Quantum Physics and Logic (QPL 2022), which was held June 27-July 1, 2022 at Wolfson College, University of Oxford, UK. QPL is an annual conference that brings…

This volume contains the papers presented at LINEARITY 2016, the Fourth International Workshop on Linearity, held on June 26, 2016 in Porto, Portugal. The workshop was a one-day satellite event of FSCD 2016, the first International…

Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The…

This book can be seen either as a text on theorem proving that uses techniques from general algebra, or else as a text on general algebra illustrated and made concrete by practical exercises in theorem proving. The book considers several…

Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the…

Despite recent advances in AI, the development of systems capable of executing complex, multi-step reasoning tasks involving multiple tools remains a significant challenge. Current benchmarks fall short in capturing the real-world…

Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI…

This volume contains the proceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), held in Saarbrucken, Germany, April 1--3, 2011. QAPL 2011 is a satellite event of the European Joint Conferences on…

In-context learning (ICL) emerges as a promising capability of large language models (LLMs) by providing them with demonstration examples to perform diverse tasks. However, the underlying mechanism of how LLMs learn from the provided…

This volume contains the final and revised versions of the papers presented at the 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011). The workshop was held in Reykjavik, Iceland, on June 9,…

This volume contains a selection of papers presented at LFMTP 2018, the 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on July 7, 2018, in Oxford, UK. The workshop was affiliated with…