On completeness of reducibility candidates as a semantics of strong normalization

On completeness of reducibility candidates as a semantics of strong normalization

This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this criterion on the classic notion of pre-Heyting algebras and m...

Full description

Bibliographic Details
Main Author:	Denis Cousineau
Format:	Article
Language:	English
Published:	Logical Methods in Computer Science e.V. 2012-02-01
Series:	Logical Methods in Computer Science
Subjects:	computer science - logic in computer science f.4.1
Online Access:	https://lmcs.episciences.org/845/pdf

Similar Items

Normalization of IZF with Replacement
by: Wojciech Moczydlowski
Published: (2008-04-01)

Classical BI: Its Semantics and Proof Theory
by: James Brotherston, et al.
Published: (2010-07-01)

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
by: Jose Espirito Santo, et al.
Published: (2009-05-01)

Intuitionistic Layered Graph Logic: Semantics and Proof Theory
by: Simon Docherty, et al.
Published: (2018-10-01)

A Normalizing Intuitionistic Set Theory with Inaccessible Sets
by: Wojciech Moczydlowski
Published: (2007-08-01)

Some model theory for the modal $\mu$-calculus: syntactic characterisations of semantic properties
by: Gaëlle Fontaine, et al.
Published: (2018-02-01)

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
by: Robert Constable, et al.
Published: (2008-09-01)

Strongly Complete Logics for Coalgebras
by: Alexander Kurz, et al.
Published: (2012-09-01)

Kripke Semantics for Martin-L\"of's Extensional Type Theory
by: Steve Awodey, et al.
Published: (2011-09-01)

The Omega Rule is $\mathbf{\Pi_{1}^{1}}$-Complete in the $\lambda\beta$-Calculus
by: Benedetto Intrigila, et al.
Published: (2009-04-01)

Ludics with repetitions (Exponentials, Interactive types and Completeness)
by: Claudia Faggian, et al.
Published: (2011-05-01)

Coalgebraic trace semantics via forgetful logics
by: Bartek Klin, et al.
Published: (2017-04-01)

On the meaning of logical completeness
by: Michele Basaldella, et al.
Published: (2010-12-01)

A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time
by: Ben Moszkowski
Published: (2012-08-01)

A proof of strong normalisation using domain theory
by: Thierry Coquand, et al.
Published: (2007-12-01)

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
by: Sylvain Conchon, et al.
Published: (2012-09-01)

Consistency and Completeness of Rewriting in the Calculus of Constructions
by: Daria Walukiewicz-Chrzaszcz, et al.
Published: (2008-09-01)

Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees
by: Amélie Gheerbrant, et al.
Published: (2012-10-01)

A Note on Shortest Developments
by: Morten Heine Sørensen
Published: (2007-11-01)

A note on the expressive power of linear orders
by: Thomas Schwentick, et al.
Published: (2011-12-01)

A proof system for graph (non)-isomorphism verification
by: Milan Banković, et al.
Published: (2023-02-01)

Axioms for Modelling Cubical Type Theory in a Topos
by: Ian Orton, et al.
Published: (2018-12-01)

Solution of a Problem of Barendregt on Sensible lambda-Theories
by: Benedetto Intrigila, et al.
Published: (2006-10-01)

Realizability algebras: a program to well order R
by: Jean-Louis Krivine
Published: (2011-08-01)

A Finite-Model-Theoretic View on Propositional Proof Complexity
by: Erich Grädel, et al.
Published: (2022-06-01)

A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic
by: Ki Yung Ahn, et al.
Published: (2021-08-01)

A System of Interaction and Structure II: The Need for Deep Inference
by: Alwen Tiu
Published: (2006-04-01)

Existential witness extraction in classical realizability and via a negative translation
by: Alexandre Miquel
Published: (2011-04-01)

Intersection Types for the lambda-mu Calculus
by: Steffen van Bakel, et al.
Published: (2018-01-01)

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
by: Stéphane Jean Eric Lengrand, et al.
Published: (2011-03-01)

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
by: Andreas Abel, et al.
Published: (2011-05-01)

Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
by: Willem Conradie, et al.
Published: (2006-03-01)

$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
by: Furio Honsell, et al.
Published: (2017-07-01)

Game semantics for first-order logic
by: Olivier Laurent
Published: (2010-10-01)

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
by: Beniamino Accattoli, et al.
Published: (2012-03-01)

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
by: Assia Mahboubi, et al.
Published: (2012-02-01)

The succinctness of first-order logic on linear orders
by: Martin Grohe, et al.
Published: (2005-06-01)

Two-Variable Logic with Two Order Relations
by: Thomas Schwentick, et al.
Published: (2012-03-01)

The Algebraic Intersection Type Unification Problem
by: Andrej Dudenhefner, et al.
Published: (2017-08-01)

Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion
by: Thomas Ehrhard, et al.
Published: (2012-10-01)