Logische Aussagen als Typen |
07.04.2021, 17:38 | Finn_ | Auf diesen Beitrag antworten » |
Logische Aussagen als Typen |
||
07.04.2021, 17:44 | Elvis | Auf diesen Beitrag antworten » |
Ich komme nicht an die Datei heran. |
||
07.04.2021, 17:48 | Finn_ | Auf diesen Beitrag antworten » |
Ist editiert. |
||
07.04.2021, 18:26 | Elvis | Auf diesen Beitrag antworten » |
Danke, insbesondere für die Literaturhinweise am Ende. |
||
11.04.2021, 01:24 | 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. |
||
22.06.2021, 12:14 | 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... |
||
Anzeige | ||
|
||
22.06.2021, 18:43 | Finn_ | Auf diesen Beitrag antworten » |
Ist korrigiert. |
|
Verwandte Themen
Die Beliebtesten » |
Die Größten » |
|
Die Neuesten » |
|