HO$$\pi $$ in Coq
| Autor: | Alan Schmitt, Guillaume Ambal, Sergueï Lenglet |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
De Bruijn sequence
Theoretical computer science Computer science Process (engineering) Carry (arithmetic) Process calculus Prove it 020207 software engineering Context (language use) 0102 computer and information sciences 02 engineering and technology 01 natural sciences Computational Theory and Mathematics 010201 computation theory & mathematics Artificial Intelligence Abstract syntax 0202 electrical engineering electronic engineering information engineering Software Scope (computer science) |
| Zdroj: | Journal of Automated Reasoning. 65:75-124 |
| ISSN: | 1573-0670 0168-7433 |
| Popis: | We present a formalization of HOπ in Coq, a process calculus where messages carry processes. Such a higher-order calculus features two very different kinds of binder: process input, similar to λ-abstraction, and name restriction, whose scope can be expanded by communication. For the latter, we compare four approaches to represent binders: locally nameless, de Bruijn indices, nominal, and Higher-Order Abstract Syntax. In each case, we formalize strong context bisimi-larity and prove it is compatible, i.e., closed under every context, using Howe's method, based on several proof schemes we developed in a previous paper. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink