Gleichungslogik und Lambda-Kalkül

What it is about

You learn the fundamentals of equation logic, term rewriting systems and untyped as well as typed lambda calculus. In the end you will be able to apply semantics and proof systems of equation logic, analyze term rewrites for correctness (termination, confluence) and program and type lambda terms as well.

What you will be able to do

• Prove confluence and termination of abstract reduction systems
• Prove equalities using rewriting and equation logic
• Define the semantics of equation logic and use it to refute equalities
• Demonstrate confluence and termination of simple rewrite systems
• Prove properties of the lambda calculus (e.g. confluence, termination)
• Express computable functions as untyped lambda terms
• Derive types for untyped lambda terms
• Translate typed lambda terms and proofs into one another

What the module consists of

• VorlesungVermittlung der Theorie im dialogischen Vortrag
• Übung/TutoriumBearbeitung von Übungsaufgaben einzeln oder in Gruppen mit Tutorunterstützung

Teaching method

• Vortrag/FrontalunterrichtExplanation and presentation of the material within the framework of the lecture
• Übungsaufgaben mit TutorunterstützungApplication and deepening of lecture material, largely written, partly computer-based