اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدProceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
378
0
0.0
(
0
)
تأليف
Claudio Sacerdoti Coen
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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 ta
sks, 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 Applicati
ons (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 se
ries 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) e
t 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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
