\(\pi\)-calculus in (Co)inductive-type theory
type: Item
instance of: scholarly article
title: \(\pi\)-calculus in (Co)inductive-type theory
zbMATH Open document ID: 0956.68095
DOI: 10.1016/S0304-3975(00)00095-5
published in: Theoretical Computer Science
publication date: 2000-12-12T00:00:00Z
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 1542391
zbMATH Keywords: higher-order abstract syntax
zbMATH Keywords: \(\pi\)-calculus
zbMATH Keywords: proof checking
zbMATH Keywords: logical frameworks
zbMATH Keywords: typed \(\pi\)-calculus
author: Furio Honsell
author: Marino Miculan
author: Ivan Scagnetto
describes a project that uses: LEGO
describes a project that uses: Coq
MaRDI profile type: Publication
cites work: Using typed lambda calculus to implement formal systems on a machine
cites work: The calculus of constructions
cites work: Automating inversion of inductive predicates in Coq
cites work: Q3024831
cites work: An application of co-inductive types in Coq: Verification of the alternating bit protocol
cites work: A framework for defining logics
cites work: A natural deduction approach to dynamic logic
cites work: A calculus of mobile processes. II
cites work: Modal logics for mobile processes
cites work: Q3999860
cites work: Q4281483
cites work: A theory of bisimulation for the \(\pi\)-calculus
cites work: A natural extension of natural deduction
cites work: Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
description: scientific article; zbMATH DE number 1542391