Logische Aussagen als Typen

Neue Frage »

Finn_ Auf diesen Beitrag antworten »
Logische Aussagen als Typen
Dem geneigten Leser möchte ich, sofern ihm die Thematik gänzlich unbekannt sein mag, meine kurzen Ausführungen in den Folien Aussagen als Typen empfehlen. Der Gegenstand ist eine in leichten Gedanken fassbare Überlegung, aus der allerdings eine Berührregion zwischen der Mathematik und der Informatik erwächst, die für das Fortschreiten der Mathematik im besonderen Maße erquicklich ist. Die tiefliegenden Zusammenhänge, welche aus dieser Überlegung entspringen, erhöhen ihre Bedeutungsschwere zudem nochmals im besonderen Maße.
Elvis Auf diesen Beitrag antworten »

Ich komme nicht an die Datei heran.
Finn_ Auf diesen Beitrag antworten »

Ist editiert.
Elvis Auf diesen Beitrag antworten »

Danke, insbesondere für die Literaturhinweise am Ende.
zweiundvierzig Auf diesen Beitrag antworten »

Coq basiert auf dem Calculus of (co-/inductive) Constructions (CoC/CIC), entwickelt von Coquand, Huet und Paulin-Mohring:
Coquand, Huet: The calculus of constructions, Information and Computation. Vol 76, Issues 2–3, 1988
Coquand, Paulin-Mohring: Inductively defined types. Proc. COLOG 1988
Paulin-Mohring: Introduction to the Calculus of Inductive Constructions (2015)

Intuitionistische Typentheorie mit induktiven Identitätstypen geht zurück auf
Martin-Löf: An Intuitionistic Theory of Types: Predicative Part. Logic Colloquium 1973,
mit der heute geläufigen Reformulierung von
Paulin-Mohring: Inductive definitions in the system Coq rules and properties. TLCA 1993.
zweiundvierzig Auf diesen Beitrag antworten »

Noch eine kleine Anmerkung: In der Curry-Howard-Tabelle gibt es einen Typo, es sollten die Begriffe "Summe" und "Produkt" vertauscht sein. (Führt vermutlich nicht zu ernsthaften Verwechslungen, aber wenn es mir schonmal auffällt...smile
 
 
Finn_ Auf diesen Beitrag antworten »

Ist korrigiert.
Neue Frage »
Antworten »



Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »