nominal

      PVS and Coq specifications and formalisations for the Nominal Setting

Description

Welcome! This page contains PVS and Coq specifications and formalisations for the nominal setting, done by the computer science theory group of University of Brasília (UnB) - Brazil.

The nominal theory in PVS, also available at the PVS NASAlib.

Theory in Coq:

Download

Related work

Work in Progress

Contact

The main authors are Mauricio Ayala-Rincón, Maribel Fernandez, Ana Cristina Rocha Oliveira , Washington de Carvalho Segundo, Gabriel Ferreira Silva, Daniele Nantes Sobrinho and Deivid Vale.