addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramFill 1linklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo

Agda — Mit starken Typen abhängen

I'm happy to announce that we have a speaker for our third meetup!

Joachim Breitner will give a demonstration of Agda, which is both a a proof assistant and functional, dependently-typed programming language.

Here is the abstract:

Programming languages are a dime a dozen; this time we want to have a look at a language less well-known than maybe C, Java or PHP. More precisely, it is about Agda, which is both a functional language (like Haskell) and an interactive theorem prover (like Coq).

This talk is no tutorial, but a demonstartion: Joachim will simply start his editor and work on a small problem, live. We will see how we can precisely model our requirements by defining data types in a dependent type system; we will learn how to replace exception handling and how we can prove the correctness of an application in Agda itself.

–––––

Programmiersprachen gibt es wie Sand am Meer; wir wollen hier an Stränden sandeln die etwas weiter weg der üblichen touristischen Hochburgen wie C, Java oder PHP sind. Genau gesagt geht es um Agda, was gleichzeitig eine funktionale Programmiersprache (wie Haskell) und ein Theorembeweiser (wie Coq) ist.

Der Vortrag ist kein Tutorial, sondern eine Demonstration: Joachim wird einfach den Editor starten und ein kleines Problem live bearbeiten. Dabei wird man sehen wie man mit einem abhängigen Typsystem sich Datentypen definiert, die exakt das darstellen, was man braucht, und wie man damit Ausnahmebehandlungen ersetzt und wie man in Agda selbst die Korrektheit des Programms beweist.

The presentation will be given in English. (Joachim is able to give this talk in both German and English, so if the audience is more comfortable with German, the language can be adapted.)

 

Schedule

18:30 Welcome and organizational matters

18:45 Joachim Breitner: Agda – Programming with the strong type of types

The talk will run for an hour (or slightly longer).

After the meetup, we plan to go to the Pizzahaus for some interesting conversations and drinks.

The company is located in the Hoepfner-Burghof, on the third floor. You'll see signs posted to help you find your way.

Join or login to comment.

6 went

Our Sponsors

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy