scholarly journals Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts

2001 ◽  
pp. 364-378 ◽  
Author(s):  
Christine Röckl ◽  
Daniel Hirschkoff ◽  
Stefan Berghofer
Keyword(s):  
Higher Order ◽  
Abstract Syntax ◽  
Π Calculus

A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis

2003 ◽  
Vol 13 (2) ◽  
pp. 415-451 ◽  
Author(s):  
CHRISTINE RÖCKL ◽  
DANIEL HIRSCHKOFF
Keyword(s):  
General Purpose ◽  
Higher Order ◽  
Abstract Syntax ◽  
Proof Technique ◽  
Syntax Analysis ◽  
Closed World Assumption ◽  
Logical Frameworks ◽  
Closed World ◽  
Higher Order Terms ◽  
Π Calculus

This paper discusses an application of the higher-order abstract syntax technique to general-purpose theorem proving, yielding shallow embeddings of the binders of formalized languages. Higher-order abstract syntax has been applied with success in specialized logical frameworks which satisfy a closed-world assumption. As more general environments (like Isabelle/HOL or Coq) do not support this closed-world assumption, higher-order abstract syntax may yield exotic terms, that is, datatypes may produce more terms than there should actually be in the language. The work at hand demonstrates how such exotic terms can be eliminated by means of a two-level well-formedness predicate, further preparing the ground for an implementation of structural induction in terms of rule induction, and hence providing fully-fledged syntax analysis. In order to apply and justify well-formedness predicates, the paper develops a proof technique based on a combination of instantiations and reabstractions of higher-order terms. As an application, syntactic principles like the theory of contexts (as introduced by Honsell, Miculan, and Scagnetto) are derived, and adequacy of the predicates is shown, both within a formalization of the π-calculus in Isabelle/HOL.

scholarly journals Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs

10.29007/jqtz ◽  
2018 ◽  
Author(s):  
Nada Habli ◽  
Amy P. Felty
Keyword(s):  
Programming Languages ◽  
Automatic Generation ◽  
Higher Order ◽  
Specification Language ◽  
Proof Assistants ◽  
Abstract Syntax ◽  
Formal Systems ◽  
Ongoing Work ◽  
General Specification ◽  
Automated Proof

We describe ongoing work on building an environment to support reasoning in proof assistants that represent formal systems using higher-order abstract syntax (HOAS). We use a simple and general specification language whose syntax supports HOAS. Using this language, we can encode the syntax and inference rules of a variety of formal systems, such as programming languages and logics. We describe our tool, implemented in OCaml, which parses this syntax, and translates it to a Coq library that includes definitions and hints for aiding automated proof in the Hybrid system. Hybrid itself is implemented in Coq, and designed specifically to reason about such formal systems. Given an input specification, the library that is automatically generated by our tool imports the general Hybrid library and adds definitions and hints for aiding automated proof in Hybrid about the specific programming language or logic defined in the specification. This work is part of a larger project to compare reasoning in systems supporting HOAS. Our current work focuses on Hybrid, Abella, Twelf, and Beluga, and the specification language is designed to be general enough to allow the automatic generation of libraries for all of these systems from a single specification.

scholarly journals Light logics and higher-order processes

2014 ◽  
Vol 26 (6) ◽  
pp. 969-992 ◽  
Author(s):  
UGO DAL LAGO ◽  
SIMONE MARTINI ◽  
DAVIDE SANGIORGI
Keyword(s):  
Polynomial Time ◽  
Linear Logic ◽  
Higher Order ◽  
Resource Control ◽  
Process Algebras ◽  
Π Calculus ◽  
Soft Processes

We show that the techniques for resource control that have been developed by the so-calledlight logicscan be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

scholarly journals Reversibility in the higher-order π-calculus

2016 ◽  
Vol 625 ◽  
pp. 25-84 ◽  
Author(s):  
Ivan Lanese ◽  
Claudio Antares Mezzina ◽  
Jean-Bernard Stefani
Keyword(s):  
Higher Order ◽  
Π Calculus

scholarly journals Primitive recursion for higher-order abstract syntax

2001 ◽  
Vol 266 (1-2) ◽  
pp. 1-57 ◽  
Author(s):  
Carsten Schürmann ◽  
Joëlle Despeyroux ◽  
Frank Pfenning
Keyword(s):  
Higher Order ◽  
Abstract Syntax ◽  
Primitive Recursion
Sign in / Sign up

Export Citation Format

Share Document