NDLI: Implicative formulae in the proofs of computations' analogy

Please wait, while we are loading the content...

On laziness and optimality in lambda interpreters: tools for specification and analysis

An algorithm for optimal lambda calculus reduction

Explicit substitutions

A formulae-as-type notion of control

Implicative formulae in the proofs of computations' analogy

Computable process

The chemical abstract machine

Interaction nets

Toward a typed foundation for method specialization and inheritance

Inheritance is not subtyping

A type system for Smalltalk

A relationship between abstract interpretation and projection analysis

On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications

Small domains spell fast strictness analysis

An efficient hybrid algorithm for incremental data flow analysis

A finite presentation theorem for approximating logic programs

Program transformation in the presence of errors

Making asynchronous parallelism safe for the world

Concurrent constraint programming

Parallelism in logic programs

Combining generational and conservative garbage collection: framework and implementations

Scheduling time-critical instructions on RISC machines

Automata-driven indexing of Prolog clauses

Fairness and hyperfairness in multi-party interactions

Relating total and partial correctness interpretations of non-deterministic programs

On oraclizable networks and Kahn's principle

On the relations computable by a class of concurrent automata

Higher-order modules and the phase distinction

Safe run-time overloading

Quasi-static typing

Deciding ML typability is complete for deterministic exponential time

Implicative formulae in the proofs of computations' analogy

Content Provider	ACM Digital Library
Author	Gorrieri, Roberto Ferrari, Gian Luigi Asperti, Andrea
Abstract	In [As87] a correspondence between the subset of Linear Logic [Gi86] involving the conjunctive tensor product only and Place/Transition Petri Nets [Rei85] is established. In this correspondence, formulae are regarded as distributed states and provable sequents are computations in the net. Developing this idea, Martì-Oliet and Meseguer [MaM89] have suggested that all the other computations of Linear Logic, which do not have an immediate correspondence with Petri Nets, should be regarded as “gedanken” or idealized processes, providing a richer language for the specification and the study of properties of distributed computations. In this paper we apply this program to the fundamental connective of linear implication. We prove that the introduction of linear implication allows us to observe the net at a lower, more decentralized level of atomicity, where the preemption of each resource needed for the firing of a transition is represented as a separate move. We give a conservative theorem relating computations at different levels of abstraction. The categorical semantics establishes a tight correspondence among Petri nets, monoidal closed categories and tensor theories, reminiscent of the well known relation among functional languages, Cartesian closed categories and intuitionistic logic [LS86]. The identification of computations in the categorical model naturally suggests the generalisation of the notion of process [DMM89] at the lower level of atomicity.
Starting Page	59
Ending Page	71
Page Count	13
File Format	PDF
ISBN	0897913434
DOI	10.1145/96709.96715
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1989-12-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Implicative formulae in the vroofs as computations ” analogy.

How to delegate computations: the power of no-signaling proofs

28. Proofs of Two Formulae in Spherical Trigonometry

Proofs and computations.

Denotations for classical proofs – Preliminary results –

453. Geometrical Proofs of Some Triangle Formulae

Analogy Makes Proofs Feasible

Mixing Computations and Proofs

An Upper Bound on the Space Complexity of Random Formulae in Resolution

Implicative formulae in the proofs of computations' analogy

Similar Documents

Implicative formulae in the vroofs as computations ” analogy.

How to delegate computations: the power of no-signaling proofs

28. Proofs of Two Formulae in Spherical Trigonometry

Proofs and computations.

Denotations for classical proofs – Preliminary results –

453. Geometrical Proofs of Some Triangle Formulae

Analogy Makes Proofs Feasible

Mixing Computations and Proofs

An Upper Bound on the Space Complexity of Random Formulae in Resolution

Implicative formulae in the proofs of computations' analogy