# Proofs and types

@inproceedings{Girard1989ProofsAT, title={Proofs and types}, author={Jean-Yves Girard and Paul Taylor and Yves Lafont}, year={1989} }

Sense, denotation and semantics natural deduction the Curry-Howard isomorphism the normalisation theorem Godel's system T coherence spaces denotational semantics of T sums in natural deduction system F coherence semantics of the sum cut elimination (Hauptsatz) strong normalisation for F representation theorem semantics of System F what is linear logic?

#### 1,920 Citations

Semantics and Proof Theory of an Intuitionistic Modal Sequent Calculus

- 2009

We prove soundness and adequacy for an intuitionistic modal sequent calculus with the modal Heyting algebra semantics presented in Hilken [7]. We produce a cut-elimination for this calculus. For… Expand

Intuitionistic linear logic and partial correctness

- Mathematics, Computer Science
- Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
- 2001

A Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare logic and is a noncommutative intuitionistic linear logic that proves soundness and completeness over relational and trace models. Expand

Computational Types from a Logical Perspective

- Computer Science
- J. Funct. Program.
- 1998

This paper shows that the computational lambda calculus also arises naturally as the term calculus corresponding to a novel intuitionistic modal propositional logic and gives natural deduction, sequent calculus and Hilbert-style presentations of this logic and proves strong normalisation and confluence results. Expand

A Non-uniform Finitary Relational Semantics of System T

- Computer Science, Mathematics
- FICS
- 2009

Although iteration and recursion operators in the denotational semantics of typed λ-calculi derived from the multiset relational model of linear logic are defined as fixpoints of typed functionals, they are proved finitary in the sense of Ehrhard's finiteness spaces. Expand

A natural deduction system for bundled branching time logic

- Mathematics, Computer Science
- J. Appl. Non Class. Logics
- 2013

A natural deduction system for the until-free subsystem of the branching time logic that provides a suitable semantics for the system and proves that it is sound and weakly complete with respect to such semantics. Expand

Unified Semantics for Modality and Lambda-terms via Proof Polynomials

- Mathematics
- 2002

It is shown that the modal logic S4, simple-calculus and modal-calculus admit a realization in a very simple propositional logical system LP, which has an exact provability semantics. In LP both… Expand

Gödel logic: From natural deduction to parallel computation

- Computer Science, Mathematics
- 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- 2017

The results provide a computational interpretation of G, thus proving A. Avron's 1991 thesis, and the resulting functional language extends the simply typed λ-calculus via a synchronous communication mechanism between parallel processes, which increases its expressive power. Expand

Permutability of Proofs in Intuitionistic Sequent Calculi

- Mathematics, Computer Science
- Theor. Comput. Sci.
- 1999

It is proved, using a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic are inter-permutable iff they determine the same natural deduction. Expand

On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains

- Mathematics, Computer Science
- CL&C
- 2018

The methods of natural deduction and Curry-Howard correspondence are used to provide a simple computational interpretation of the logic of constant domains, a classically valid statement which implies the excluded middle over decidable formulas. Expand

Proof-terms for classical and intuitionistic resolution

- Computer Science
- J. Log. Comput.
- 2000

We exploit a system of realizers for classical logic, and a translation from resolution into the sequent calculus, to assess the intuitionistic force of classical resolution for a fragment of… Expand

#### References

SHOWING 1-10 OF 65 REFERENCES

Stable Models of Typed lambda-Calculi

- Computer Science
- ICALP
- 1978

It is shown that Milner's fully abstract model of Plotkin's PCP language only contains stable functions, and new model constructions from a notion of stable function are presented. Expand

The lambda calculus - its syntax and semantics

- Mathematics, Computer Science
- Studies in logic and the foundations of mathematics
- 1985

This chapter discusses the theory and practice of reduction in the context of classical Lambda Calculus, as well as some of the theories and practices used in the development of modern lambda calculus. Expand

Proof Theory and Logical Complexity

- Mathematics
- 1989

Introduction: Elementary Proof Theory. The Fall of Hilbert's Program. Hilbert's Program. Recursive Functions. The First Incompleteness Theorem. The Second Incompleteness Theorem. Exercises. Annex:… Expand

Linear Logic and Lazy Computation

- Computer Science
- TAPSOFT, Vol.2
- 1987

Recently, J.Y. Girard discovered that usual logical connectors such as ⇒ (implication) could be broken up into more elementary linear connectors, providing a new linear logic where hypothesis are used once and only once. Expand

Domain Theory in Logical Form

- Computer Science
- LICS
- 1987

Domain theory, the mathematical theory of computation introduced by Scott as a foundation for detonational semantics, and the theory of concurrency and systems behaviour developed by Milner, Hennesy based on operational semantics are introduced. Expand

The System F of Variable Types, Fifteen Years Later

- Mathematics, Computer Science
- Theor. Comput. Sci.
- 1986

A semantics based on the category-theoretic idea of direct limit is developed, so that the behaviour of a variable type on any domain is determined by its behaviour on finite ones, thus getting rid of the circularity of variable types. Expand

Reasoning about functional programs and complexity classes associated with type disciplines

- Computer Science, Mathematics
- 24th Annual Symposium on Foundations of Computer Science (sfcs 1983)
- 1983

This work presents a method of reasoning directly about functional programs in Second-Order Logic, based on the use of explicit second-order definitions for inductively defined data-types, which implies that, for functions defined over inductivelydefined types, the property of being proved everywhere-defined in Second -Order Logic is equivalent to theproperty of being representable in the Second- order Lambda Calculus. Expand

The Linear Abstract Machine (Corrigenda)

- Computer Science
- Theor. Comput. Sci.
- 1988

Abstract Linear Logic [6] provides a refinement of functional programming and suggests a new implementation technique, with the following features: • a synthesis of strict and lazy evaluation, • a… Expand

Contracting proofs to programs

- Computer Science
- 1989

A family of homomorphisms that contract natural deductions into typed ^-expressions, with the property that a convergence proof for an untyped program for function / is contracted to a typed program for / is described. Expand

The formulae-as-types notion of construction

- Computer Science
- 1969

The ultimate goal was to develop a notion of construction suitable for the interpretation of intuitionistic mathematics, so the use of the word construction is not very appropriate, but the terminology has been kept in order to preserve the original title. Expand