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.
翻译:逻辑框架和元语言是代表、实施和推理各种逻辑和计算机科学的推理系统的共同基础,其设计、实施和用于推理任务,从软件的正确性到正规系统的特性,在过去二十年中一直是大量研究的焦点,这次讲习班汇集了设计者、实施者和从业人员,讨论与逻辑框架的结构和效用有关系的各个方面,包括处理可变的、有约束性的、感性、共导性的推理技术以及推理过程的清晰度和清晰度。