Project

Back to overview

Computational structure of higher-order sequent calculi

Applicant McKinley Richard
Number 145747
Funding scheme Ambizione
Research institution Institut für Informatik Universität Bern
Institution of higher education University of Berne - BE
Main discipline Information Technology
Start/End 01.03.2013 - 28.02.2014
Approved amount 151'976.00
Show all

All Disciplines (2)

Discipline
Information Technology
Mathematics

Keywords (3)

Logic; Process calculus; Proof theory

Lay Summary (German)

Lead
Wir suchen einem rechnerischen Interpretation klassischer Beweise, mittels der definition von Sequenzenkalküle mit aspekten der höhere Ordnung.
Lay summary
Die Curry-Howard Korrespondenz, auch bekannt als die
Beweise-as-Programme Korrespondenz, ist die Beobachtung, dass
Beweise und Programme gibt zwei Möglichkeiten der Darstellung der gleichen mathematischen
Objekte. 

Das Projekt `` Computational Struktur der klassischen Dualität'', finanziert
durch den SNF unter dem Ambizione Regelung wurde gegründet, um
Beiträge zum Verständnis der klassischen Logik in die
Beweise-as-Programme Paradigma. Es gibt kein allgemeines Verständnis der
klassischen Beweise als Programme: stattdessen gibt es eine Vielzahl von
Beweis-Kalküle für klassische Logik, jede mit ihrer eigenen unterschiedlichen
Computational Lesen. Das Projekt zielt darauf ab, eine einheitliche Sprache zu finden
zur Expression dieser verschiedenen Proof-Systeme, und dadurch ein
einheitliche Präsentation der rechnerische Bedeutung der klassischen Beweis.

Unser Erfolg in dieser Richtung aus einer unerwarteten Richtung kommen,
die sich aus der folgenden Erkenntnis: die robuste Rechenleistung
Verständnis intuitionistic Beweise als funktionale Programme entsteht
denn wir können sofort verstehen, eine natürliche Abzug mit
die üblichen Einführung / Beseitigung Regeln als typisierte Version von a
höherer Ordnung funktionale Programmiersprache. Auf der anderen Seite,
nachfolgenden Systemen fehlt eine unmittelbare Interpretation als rechnerische
Objekte. Das heißt, die Frage in das Projekt gebeten umgeleitet werden kann,
statt der Suche nach einem rechnerischen Interpretation klassischer
nachfolgenden Beweise, können wir für eine rechnerische Auslegung Besichtigen
allgemeine Klasse von nachfolgenden Systemen, von denen die verschiedenen klassischen
nachfolgenden Kalküle sind Instanzen.
Direct link to Lay Summary Last update: 03.06.2013

Responsible applicant and co-applicants

Employees

Collaboration

Group / person Country
Types of collaboration
Department of Computer Science, University of Bath Great Britain and Northern Ireland (Europe)
- in-depth/constructive exchanges on approaches, methods or results
PPS, Université Paris VII France (Europe)
- in-depth/constructive exchanges on approaches, methods or results

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
Theory and Application of Formal Proofs Talk given at a conference Higher-order sequent proofs, higher-order nets 05.11.2013 Palaiseux, France McKinley Richard;


Associated projects

Number Title Start Funding scheme
126422 Computational Structure of Classical Duality 01.03.2010 Ambizione

Abstract

Die Curry-Howard Korrespondenz, auch bekannt als dieBeweise-as-Programme Korrespondenz, ist die Beobachtung, dassBeweise und Programme gibt zwei Möglichkeiten der Darstellung der gleichen mathematischenObjekte. Das am weitesten entwickelte Korrespondenz dieser Art istzwischen intuitionistic Logik (etwa, Logik, ohne das Gesetz derausgeschlossen Mitte) und typisierte Lambda-Kalkül, wo Beweise in natürlichenAbzug zu prototypischen funktionale Programme entsprechen. Ein BeweisAbleiten einer Formel A aus einem Satz von Annahmen G angezeigt werdenals ein Programm mit Parametern G, Ableiten von Daten des Typs A.diese Einstellung ist Berechnung Normalisierung: ein Prozess derEntfernen ``'' Umwege von einem Beweis, der seine logische vereinfachtStruktur. Die Korrespondenz gilt für propositionale erster Ordnungund höherer Ordnung Logiken / Typ Theorien und hat die Quelle derzahlreiche nützliche Einblicke sowohl in Theorie und Beweis ProgrammierspracheDesign. Insbesondere die einheitliche semantische TheorieNachweise / Programme in dieser Einstellung (Interpretation in einkartesischen geschlossenen Kategorie) gibt eine Möglichkeit zu sagen, wenn zweiBeweise (oder zwei Programme) im wesentlichen gleich sind.Das Projekt `` Computational Struktur der klassischen Dualität'', finanziertdurch den SNF unter dem Ambizione Regelung wurde gegründet, umBeiträge zum Verständnis der klassischen Logik in dieBeweise-as-Programme Paradigma. Es gibt kein allgemeines Verständnis derklassischen Beweise als Programme: stattdessen gibt es eine Vielzahl vonBeweis-Kalküle für klassische Logik, jede mit ihrer eigenen unterschiedlichenComputational Lesen. Das Projekt zielt darauf ab, eine einheitliche Sprache zu findenzur Expression dieser verschiedenen Proof-Systeme, und dadurch eineinheitliche Präsentation der rechnerische Bedeutung der klassischen Beweis.Unser Erfolg in dieser Richtung aus einer unerwarteten Richtung kommen,die sich aus der folgenden Erkenntnis: die robuste RechenleistungVerständnis intuitionistic Beweise als funktionale Programme entstehtdenn wir können sofort verstehen, eine natürliche Abzug mitdie üblichen Einführung / Beseitigung Regeln als typisierte Version von ahöherer Ordnung funktionale Programmiersprache. Auf der anderen Seite,nachfolgenden Systemen fehlt eine unmittelbare Interpretation als rechnerischeObjekte. Das heißt, die Frage in das Projekt gebeten umgeleitet werden kann,statt der Suche nach einem rechnerischen Interpretation klassischernachfolgenden Beweise, können wir für eine rechnerische Auslegung Besichtigenallgemeine Klasse von nachfolgenden Systemen, von denen die verschiedenen klassischennachfolgenden Kalküle sind Instanzen.
-