Related papers: Proceedings Types for Proofs and Programs, Revised…
The Curry-Howard correspondence is about a relationship between types and programs on the one hand and propositions and proofs on the other. The implications for programming language design and program verification is an active field of…
This volume contains the proceedings of the 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA'14). The workshop was held in Singapore on May 13th, 2014, as a satellite event of the 19th International Symposium on…
In concurrent and distributed systems, software components are expected to communicate according to predetermined protocols and APIs - and if a component does not observe them, the system's reliability is compromised. Furthermore, isolating…
This volume contains the proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010) which took place on July 15 in Edinburgh, UK. This workshop was held as a satellite workshop of the International…
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a…
The Theory-Software Translation Workshop, held in New Orleans in February 2019, explored in depth the process of both instantiating theory in software - for example, implementing a mathematical model in code as part of a simulation - and…
Our scientific knowledge is increasingly built on software output. User code which defines data analysis pipelines and computational models is essential for research in the natural and social sciences, but little is known about how to…
This volume contains the formal proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), held on 8th September 2017 in Oxford, United Kingdom, and affiliated with the…
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to…
Algorithmic reasoning refers to the ability to understand the complex patterns behind the problem and decompose them into a sequence of reasoning steps towards the solution. Such nature of algorithmic reasoning makes it a challenge for…
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher order…
PLACES 2012 (full title: Programming Language Approaches to Concurrency- and Communication-Centric Software) is the fifth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop…
This volume contains the papers selected among those which were presented at the 3rd International Workshop on Verification and Program Transformation (VPT 2015) held in London, UK, on April 11th, 2015. Previous editions of the Workshop…
This volume contains the proceedings of ACL2 2011, the International Workshop on the ACL2 Theorem Prover and its Applications. The workshop was held in Austin, Texas, USA, on November 3-4 2011. ACL2 2011 is the tenth in a series of…
Large language models (LLMs) have achieved notable success in code generation. However, they still frequently produce uncompilable output because their next-token inference procedure does not model formal aspects of code. Although…
The Message Passing Interface (MPI) framework is widely used in implementing imperative pro- grams that exhibit a high degree of parallelism. The PARTYPES approach proposes a behavioural type discipline for MPI-like programs in which a type…
Methods for Modalities is a series aimed at bringing together researchers interested in developing proof methods, verification methods, algorithms and tools based on modal logic. Here the term "modal logics" is conceived broadly, including…
This volume contains a selection of the papers presented at the Ninth International Workshop on Developments in Computational Models (DCM 2013) held in Buenos Aires, Argentina on 26th August 2013, as a satellite event of CONCUR 2013.…
The aim of the FESCA workshop is to bring together both young and senior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated…
This volume consists of papers presented at the Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK) held at the University of Liverpool, UK, from July 24 to 26, 2017. TARK conferences bring together researchers…