Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic

Author： Okada M.  

Publisher： Elsevier

ISSN： 0304-3975

Source： Theoretical Computer Science, Vol.227, Iss.1, 1999-09, pp. : 333-396

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

Related content

Cut-elimination for a logic with definitions and induction

By McDowell R.   Miller D.  

Theoretical Computer Science, Vol. 232, Iss. 1, 2000-02 ,pp. : 91-119

Elsevier

Access to resources Recommend Favorite

A semantic proof of strong cut-admissibility for first-order Gdel logic

By Lahav Ori   Avron Arnon  

Journal of Logic and Computation, Vol. 23, Iss. 1, 2013-02 ,pp. : 59-86

Oxford University Press

Access to resources Recommend Favorite

Proofs as computations in linear logic

By Delzanno G.   Martelli M.  

Theoretical Computer Science, Vol. 258, Iss. 1, 2001-05 ,pp. : 269-297

Elsevier

Access to resources Recommend Favorite

On proof normalization in linear logic

By Perrier G.  

Theoretical Computer Science, Vol. 206, Iss. 1, 1998-10 ,pp. : 353-354

Elsevier

Access to resources Recommend Favorite

Verification of FPGA Layout Generators in Higher-Order Logic

By Pell Oliver  

Journal of Automated Reasoning, Vol. 37, Iss. 1-2, 2006-08 ,pp. : 117-152

Springer Publishing Company

Access to resources Recommend Favorite