Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userProceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
378
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Claudio Sacerdoti Coen
Ask ChatGPT about the research
No Arabic abstract
This volume contains a selection of papers presented at LFMTP 2020, the 15th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held the 29-30th of June, 2019, using the Zoom video conferencing tool due to COVID restrictions. Officially the workshop was held in Paris, France, and it was affiliated with IJCAR 2020, FSCD 2020 and many other satellite events. Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
rate research
Read More
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop brings together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
This volume contains a final and revised selection of papers presented at the Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), held in Vienna (Austria) on July 18th, affiliated with TLCA 2014, Typed Lambda Calculi and Applications (held jointly with RTA, Rewriting Techniques and Applications) as part of FLoC and the Vienna Summer of Logic (VSL) 2014. Intersection types have been introduced in the late 1970s as a language for describing properties of lambda calculus which were not captured by all previous type systems. They provided the first characterisation of strongly normalising lambda terms and have become a powerful syntactic and semantic tool for analysing various normalisation properties as well as lambda models. Over the years the scope of research on intersection types has broadened. Recently, there have been a number of breakthroughs in the use of intersection types and similar technology for practical purposes such as program analysis, verification and concurrency, and program synthesis. The aim of the ITRS workshop series is to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches (e.g., union types, refinement types, behavioral types).
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 HCVS series of workshops aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis. Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
This volume contains the post-proceedings of the 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS), which took place virtually due to Covid-19 pandemic as an affiliated workshop of ETAPS.
The proceedings consist of a keynote paper by Alberto followed by 6 invited papers written by Lorenzo Clemente (U. Warsaw), Alain Finkel (U. Paris-Saclay), John Gallagher (Roskilde U. and IMDEA Software Institute) et al., Neil Jones (U. Copenhagen) et al., Michael Leuschel (Heinrich-Heine U.) and Maurizio Proietti (IASI-CNR) et al.. These invited papers are followed by 4 regular papers accepted at VPT 2020 and the papers of HCVS 2020 which consist of three contributed papers and an invited paper on the third competition of solvers for Constrained Horn Clauses. In addition, the abstracts (in HTML format) of 3 invited talks at VPT 2020 by Andrzej Skowron (U. Warsaw), Sophie Renault (EPO) and Moa Johansson (Chalmers U.), are included.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
