WG 2.11 - User contributions [en]

WG211/M24Amin

2024-12-25T13:32:26Z

Nada: abstract

Extrapolating from my old [https://pl-ai-seminar.seas.harvard.edu/ 2020 PL+AI graduate seminar],
LLMs are good at:
* Neural-Guided Search
* Semantic Parsing: translating from natural language to formal language.

I showed experiments:
* 0. [https://metareflection.seas.harvard.edu/openai/ ChatGPT with formal tools]
* 1. [https://github.com/namin/llm-verified-with-monte-carlo-tree-search VerMCTS]
* 2. [https://github.com/metareflection/dafny-annotator Dafny-annotator] led by Gabriel Poesia at Stanford
* 3. [https://github.com/namin/dafny-sketcher Dafny Sketcher]

I am co-chairing [https://2025.ecoop.org/home/gpce-2025 GPCE 2025], and we will expand the scope of "generative" programming.

WG211/M24Schedule

2024-12-03T06:01:08Z

Nada: /* Talks */

= IFIP Working Group 2.11, Twenty-fourth Meeting =

== December 3rd (Tues) - 6th (Fri) in Edinburgh, Scotland, UK ==

The meeting will be hosted by [https://www.denotational.co.uk/ Ohad Kammar], who will write in the first person in the remainder.

The meeting will last 3.5 days; the first three days (Tues-Thur) will
be full-day whereas the last day (Fri) will be a half-day session.

=== Venue ===

[https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0401_01_1.07 Althaus-Reid Room, 1.07] ([http://exhibition.div.ed.ac.uk/rooms-renamed-in-honour-of-two-inspirational-female-theologians/ named after the theologian Marcella Althaus-Reid])

New College 
School of Divinity 
The University of Edinburgh 
Central Campus 
1 Mound Place 
Edinburgh EH1 2LU

This is unfortunately '''not''' the School of Informatics, which is about 15 minutes walk south from this venue.

A [https://maps.app.goo.gl/oCXGNCb2ax68WS6B6/ Google map] with the venue, hotels, and meeting-relevant locations.

==== WiFi Access ====

* '''eduroam.''' If you have eduroam credentials, you may use them to access the eduroam network while at Edinburgh.

* '''guest account.''' If you know that eduroam will not work for you, I can set you up with a guest account. Please indicate that you will definitely need a guest account in your registration form. You can always let me know after registration whether you need one, including during the meeting. Guests must abide by the [https://vpnreg.ucs.ed.ac.uk/admin/compregs.pdf computing regulations].

* '''Visit-Ed.''' If eduroam does not work for you and you don't have a guest account, you can try using the [https://www.ed.ac.uk/information-services/computing/desktop-personal/wifi-networking/guest-alumni-wifi-access Visit-Ed service] described in the middle of that page. It requires registration by Facebook, LinkedIn, WhatsApp, or text message (international numbers included).

==== Workspace ====

A quiet area for shared use is available in the [https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0401_01_1.09 Porteous Room 1.09]
(you can read more about it
[https://exhibition.div.ed.ac.uk/porteous%E2%80%AFroom/ here]) on the
same floor as the main room.

== Travel ==

=== Travel to Edinburgh ===

==== Air ====

[https://www.edinburghairport.com/ Edinburgh Airport] is located
approximately 8 miles away from the city centre.

The [https://edinburghtrams.com/ Edinburgh tram] runs from the
airport every 7 minutes, the last tram from the airport leaves after
22:30 (see tram webpage).

The [https://airlink100.co.uk/ Airlink bus] (service 100) runs
between the airport and the city centre, reaching Waverley Bridge
railway station in 25 minutes. The route to and from the airport runs
24 hours a day every 10 minutes approximately during the day.

Most advance hire taxi companies will offer an airport pick-up
service. [https://www.taxis-edinburgh.co.uk/ Here's one], but any will
do. There's also a taxi hailing stand at the airport, follow the signs.

You can also fly into another main UK city and continue to Edinburgh by [[#Train|train]].

==== Train ====

Edinburgh is well-connected to most other main UK cities. There are a
few faster trains from London (about 4h25min) every day. You can use [https://www.nationalrail.co.uk/ National Rail] to plan your trip and link you to the appropriate provider.

I have enjoyed taking the Eurostar from the main continent to London. There is also the [https://www.sleeper.scot/ Caledonian Sleeper] that can get you to Edinburgh or London by 7am very slowly overnight.

=== Travel around Edinburgh ===

Edinburgh is somewhat hilly and the venue is located [https://upload.wikimedia.org/wikipedia/commons/f/ff/The_Mound%2C_Edinburgh%2C_18_September_2014.jpg up a slope].
If that is not a problem, then Edinburgh is quite walkable.

Public transportation is available. Check out [https://transportforedinburgh.com/ Transport for Edinburgh] for all the details.

* Buses. [https://www.lothianbuses.com/ Lothian buses] operates many of the relevant buses. You can pay contactless with a card or app and there's a capped pay program ('TapTapCap'). Here's the [https://www.lothianbuses.com/wp-content/uploads/2024/09/Network_Map_240908.pdf map], but I usually use Google maps for directions.

* Taxis. You can usually just hail a black cab from anywhere in the centre, see their [https://www.taxis-edinburgh.co.uk/ webpage] for advance bookings. Your favourite search engine will provide other taxi companies.

* Tram. The [https://edinburghtrams.com/ Edinburgh tram] stops fairly close to the venue, so can be an easy way to the venue.

* Uber operates in Edinburgh.

== Accommodation ==

The venue is located quite centrally, with many hotels nearby. Here are some 4-star and 3-star suggestions nearby, but you'll probably find something charming by your own (just watch out for scams). The tram and buses make it easy to also stay somewhere away from the centre and commute in if you prefer.

Hotel suggestions:
* [https://www.apexhotels.co.uk/destinations/edinburgh/apex-city-of-edinburgh-hotel/ Apex City of Edinburgh Hotel]. Main suggestion, slightly-up-and-steep-downhill from the venue. We have a 10% discount code, which I will email once I have it. '''Note:''' There is a slightly more full Apex hotel on the same street which I listed before, so if you want to be in the suggested hotel, make sure you're in the correct one.
* [https://www.motel-one.com/en/hotels/edinburgh/hotel-edinburgh-royal/ Motel One Edinburgh Royal]. A cheaper option, steep downhill from the venue.
* [https://www.scotsmanhotel.co.uk/ Scotsman Hotel]. A more expensive option, slightly-up-and-moderate-downhill from the venue.

== Weather ==

Edinburgh has temperate (and temperamental) climate, and currently the broadcast is 0 to 8 degrees centrigade during the day, and perhaps -1 degrees centrigade at night and in the early morning. It will be windy with gusts of wind of up to 35 mph, and potentially rainy, so make sure you dress appropriately. Locals wear waterproof/resistant clothes. Umbrellas tend to be rather useless due to the wind, one typically recognises the tourists by their futile struggles to turn inside-out umbrellas
while getting soaked.

The days are quite short in December, and you might be able to catch
the sunrise heading into the venue in the morning. I recommend
avoiding missing most of the daylight completely, e.g., make sure you go
for a short walk outside during the lunch break.

== Tourism ==

Edinburgh offers many tourist attractions and museums, and many are located centrally and close to the venue. Entrance to museums and galleries is free. Entrance to some exhibitions in the museum or gallery will require buying a separate ticket.

The meeting takes place just after [https://www.visitscotland.com/things-to-do/events/st-andrews-day Saint Andrew's Day] weekend, and Monday will be a public holiday in Scotland.
That should not affect travel, although the airport and railway might be busier than usual.

[https://www.historicenvironment.scot/about-us/news/st-andrews-day-ticket-giveaway/ Historic Environment Scotland] offer free tickets to visit some Historic Scotland attractions on Saint Andrew's day, such as the Edinburgh Castle. Registration for [https://www.historicenvironment.scot/ticket-giveaway/ free tourism tickets] opens Tuesday 12 November 10am UK time until Thursday 28 November.

If you go to the Castle, try to get there before 1pm to see them fire the Cannon.

Very near the venue is Scott Monument which you can climb, for a fee,
during the day for a stunning view. There will be a German Christmas
Market nearby I believe.

There are several hills within the city and you can easily climb up. The easiest (and closest to the venue) is [https://ewh.org.uk/calton-hill/ Calton Hill] and has a road and steps leading all the way up.

[https://www.geolsoc.org.uk/GeositesArthursSeat Arthur's Seat and the Salisbury Crags] are most visible from the centre. It takes about 1.5 hours roundtrip to get to the top. The grass can be slippery after a rain, and people can slip to their death, so wear good shoes and only climb during the day.

You can sometimes take a daytrip on a guided tour to the highlands or a whisky distillery. If you have the time, I recommend spending a few days in the former, and maybe visiting some of the latter.

I'll try to add more stuff here, especially if people send me recommendations or ask questions.

== Registration ==
Please register [https://www.epay.ed.ac.uk/conferences-and-events/college-of-science-and-engineering/school-of-informatics/informatics-events/ifip-working-group here].
After you 'Book Event', please choose either:
* '4 Day Attendee' or
* iff you're only attending partially, tick the boxes for the relevant days.

(If you plan to partially attend, please discuss with the Chairs first. I think it's somewhat unusual.)

You'll be prompted for additional details like contact details, allergies and dietary requirements after: adding to basket; proceeding to checkout; registering.

Please let me know if you have any problems. Please let me know if you won't be able to register before Thursday 28 Nov.

== Attendance ==
(Alphabetical by last name please)

* Guillaume Allais
* Nada Amin
* Sandrine Blazy
* Edwin Brady
* Jacques Carette
* Sebastian Erdweg
* Jeremy Gibbons
* Kevin Hammond
* Ohad Kammar
* Paul Kelly (on 5-6 only)
* Andras Kovacs
* Lindsey Kuper
* Julia Lawall
* Ralf Lämmel
* Sam Lindley
* James McKinna
* Peter Mosses
* Christoph Reichenbach
* Tiark Rompf
* Sven-Bodo Scholz
* Amir Shaikhha
* Friedrich Steimann
* Jeremy Yallop

=== Local Observers ===
* Greg Brown
* Justus Matthiesen
* Nachiappan Valliappan
* Robert Wright

== Talks ==

See below for the schedule (but note that the actual scheduling of talks will not be available until the meeting starts). Members: please add yourself and your topic, alphabetically ordered by surname:
| Scoped and Typed Staging by Evaluation
* Guillaume Allais [[WG211/M24Allais | Scoped and Typed Staging by Evaluation ]]
* Nada Amin [[WG211/M24Amin | Experiments in verified program synthesis with LLMs ]]
* Sandrine Blazy [[WG211/M24Blazy | A Mechanized Semantics for Dataflow Circuits ]]
* Edwin Brady [[WG211/M24Brady | "Normalisation by Compilation": Typechecking Dependent Types via the Scheme Runtime ]]
* Jacques Carette [[WG211/M24Carette | Partial Evaluation meets Denotational Semantics ]]
* Sebastian Erdweg [[WG211/M24Erdweg | Stateful Differential Operators for Incremental Computing ]]
* Jeremy Gibbons [[WG211/M24Gibbons | Continuation−Passing Style‚ Defunctionalization‚ Accumulations‚ and Associativity ]]
* Kevin Hammond [[WG211/M24Hammond | Using Formal Methods at Scale in the Delivery of a High Assurance Distributed System: the Cardano Blockchain Implementation in Haskell ]]
* Andras Kovacs [[WG211/M24Kovacs | Runtime code generation with dependent types ]]
* Lindsey Kuper [[WG211/M24Kuper | Library-Level Choreographic Programming ]]
* Ralf Lämmel [[WG211/M24Laemmel | Type Inference in a Knowledge-Graph Setting]]
* Sam Lindley [[ WG211M24Lindley | Modal Effect Types ]]
* Peter Mosses [[ WG211/M24Mosses | Denotational Semantics in Agda ]]
* Christoph Reichenbach [[ WG211/M23Reichenbach | Circular Attribute Evaluation in Reference Attribute Grammars ]]
* Tiark Rompf [[WG211/M24Rompf | Rhyme: A Data-Centric Multi-Paradigm Query Language ]]
* Amir Shaikhha [[ WG211M24Shaikhha | Democratizing Data Science by Leveraging Structure ]]
* Sven-Bodo Scholz [[WG211/M24Scholz| Hybrid Typing --- unleashing the battle between good error messages and aggressive program optimisation ]]
* Friedrich Steimann [[ WG211/M24Steimann | A really old new metatheory of software languages ]]

We will follow our usual format of interactive talks with an active audience, using a chess clock for timing, as follows. For each talk the speaker and the audience each get at most 25 minutes. The audience does not have to wait until the end of a talk to ask questions; interaction and discussion is encouraged. (But experience from previous meetings shows that it is useful to let the speaker at least finish the introduction before interrupting.) To ensure fairness, administration of the time used by each party is done using a chess clock. Operation of the clock rotates among participants. Both speaker and audience are expected to contribute to make talks and discussions engaging, interesting, and useful. Therefore, we observe a policy of no use of electronic devices during talks (other than the device the speaker uses to present slides). Bring paper and pen for making notes.

== Program / schedule ==

=== Scientific program ===

Updated nightly for the following day.

Tuesday, December 3

* 09:00 - 09:15 Assemble and welcome
** 09:15 - 10:00 Talk 01
** 10:00 - 10:45 Talk 02
* 10:45 - 11:15 Coffee break
** 11:15 - 12:00 Talk 03
* 12:00 - 14:00 Lunch and break
** 14:00 - 14:45 Talk 04
** 14:45 - 15:30 Talk 05
* 15:30 - 16:00 Coffee break
** 16:00 - 16:45 Talk 06

* 19:00 Dinner: David Bann

Wednesday, December 4

Note: if you're planning to walk to the Galleries today, bring comfortable shoes and relatively warm clothes.

* 09:00 - 09:15 Assemble and welcome
** 09:15 - 10:00 Talk 07
** 10:00 - 10:45 Talk 08
* 10:45 - 11:15 Coffee break
** 11:15 - 12:00 Talk 09
* 12:00 - 12:55 Lunch and short break
* 12:55 onwards: afternoon excursion to the Modern Art Galleries

* 19:00 Dinner: Wee Greek Kitchen

Thursday, December 5

* 08:45 - 09:05 Assemble and welcome
** 09:05 - 09:50 Talk 10
** 09:50 - 10:35 Talk 11
* 10:35 - 11:00 Coffee break
** 11:00 - 11:45 Talk 12
** 11:45 - 12:30 Talk 13
* 12:30 - 14:15 Lunch and break
** 14:15 - 15:00 Talk 14
** 15:00 - 15:45 Talk 15
* 15:45 - 17:00 Coffee break transitioning into business meeting
* 20:30 Dinner: Howie's at Waterloo Place

Friday, December 6

* 08:45 - 09:05 Assemble and welcome
** 09:05 - 09:50 Talk 16
** 09:50 - 10:35 Talk 17
* 10:35 - 11:00 Coffee break
** 11:00 - 11:45 Talk 18
** 11:45 - 12:30 Talk 19
* 12:30 - 14:15 Lunch and farewell

=== Social events ===

==== Dinners ====
* Tuesday, 19:00 December 3: [https://www.davidbann.co.uk/ David Bann] ([https://maps.app.goo.gl/6PevFCJjTn1LfbTt5 map])
* Wednesday, 19:00 December 4: [https://weegreekkitchen.co.uk/ Wee Greek Kitchen] ([https://maps.app.goo.gl/HBJab37BAV8PSQbS9 map])
* Thursday, 20:30 December 5: [https://www.howies.uk.com/venues/howies-waterloo-place/ Howie's at Waterloo Place] ([https://maps.app.goo.gl/RwfdtvHfNaRXaZYD6 map], make sure you go to the one at Waterloo Place!)

==== Excursion ====

On Wednesday afternoon, we'll ramble to the [https://www.nationalgalleries.org/visit/scottish-national-gallery-modern-art Modern Art Galleries] [https://maps.app.goo.gl/md1ZDd1XiCBuwBpS6 One] and [https://maps.app.goo.gl/fV8oSdeHQazrL2J2A Two].

Directions:
* 12:55 Arrive independently by '''Bus:''' take the [https://maps.app.goo.gl/nFEdHat3yddNQUxZ9 13 bus from Princes Street stop PU] . See [[ WG211/M24Schedule#Travel_around_Edinburgh | Travel around Edinburgh ]] section on paying your way.
* 13:00 '''Scenic route''' walk (around 1h, dress warmly), details below.

Synchronised activities:
* 13:00 '''Scenic route''': Meet outside New College for the scenic route walk. [https://maps.app.goo.gl/NNq6dFWMTRn64oqN7 Planned route]:
** Princes Street Gardens
** Queensferry Road and Dean Village
** [https://en.wikipedia.org/wiki/Water_of_Leith_Walkway Water of Leith Walkway]
** [https://www.aidsmemorial.info/memorial/id=98/life_tribute_edinburgh_aids_memorial.html Life Tribute]

* 15:00-16:15. Guided tour of [https://maps.app.goo.gl/fV8oSdeHQazrL2J2A Modern Art Gallery Two], meet Katharine and Duncan outside.

* 16:57 [https://maps.app.goo.gl/jXtfbjfkFGjhRCBd7 Bus back to Princes Street]. See [[ WG211/M24Schedule#Travel_around_Edinburgh| Travel around Edinburgh ]] section on paying your way.
* 17:00 Galleries close.

'''Warning:''' Walking from the Galleries to the Wee Greek Kitchen will be around 1h, in the dark and cold. If you choose to walk, I recommend you stop somewhere along the way to get warm again, maybe drink a cup of tea or mulled wine. Here's a route with the [https://maps.app.goo.gl/Uitqc7dCrY6eyvuj6 last possible option to do so], but feel free to duck into any nice place along the way.

==== Thursday pre-dinner activities ====

Especially if you're not attending the business meeting, there is plenty of time to spend between sunset and dinner. A nice activity can be to stroll around the [https://www.visitscotland.com/things-to-do/events/christmas-winter-festivals/edinburgh Edinburgh Chrismas Market]. It's [https://maps.app.goo.gl/MehaaffXdeehk6NMA hard to miss], and straight down from the venue, with Howie's at Waterloo Place just up the road.

WG211/M24Schedule

2024-11-28T01:27:49Z

Nada: /* Talks */

= IFIP Working Group 2.11, Twenty-fourth Meeting =

== December 3rd (Tues) - 6th (Fri) in Edinburgh, Scotland, UK ==

The meeting will be hosted by [https://www.denotational.co.uk/ Ohad Kammar], who will write in the first person in the remainder. If you want to know anything, please email me. This page is not yet finished, I'll try to add the missing information as soon as possible.

The meeting will last 3.5 days; the first three days (Tues-Thur) will
be full-day whereas the last day (Fri) will be a half-day session.

=== Venue ===

[https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0401_01_1.07 Althaus-Reid Room, 1.07] ([http://exhibition.div.ed.ac.uk/rooms-renamed-in-honour-of-two-inspirational-female-theologians/ named after the theologian Marcella Althaus-Reid])

New College 
School of Divinity 
The University of Edinburgh 
Central Campus 
1 Mound Place 
Edinburgh EH1 2LU

This is unfortunately '''not''' the School of Informatics, which is about 15 minutes walk south from this venue.

A [https://maps.app.goo.gl/oCXGNCb2ax68WS6B6/ Google map] with the venue, hotels, and meeting-relevant locations.

==== WiFi Access ====

* '''eduroam.''' If you have eduroam credentials, you may use them to access the eduroam network while at Edinburgh.

* '''guest account.''' If you know that eduroam will not work for you, I can set you up with a guest account. Please indicate that you will definitely need a guest account in your registration form. You can always let me know after registration whether you need one, including during the meeting. Guests must abide by the [https://vpnreg.ucs.ed.ac.uk/admin/compregs.pdf computing regulations].

* '''Visit-Ed.''' If eduroam does not work for you and you don't have a guest account, you can try using the [https://www.ed.ac.uk/information-services/computing/desktop-personal/wifi-networking/guest-alumni-wifi-access Visit-Ed service] described in the middle of that page. It requires registration by Facebook, LinkedIn, WhatsApp, or text message (international numbers included).

==== Workspace ====

A quiet area for shared use is available in the [https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0401_01_1.09 Porteous Room 1.09]
(you can read more about it
[https://exhibition.div.ed.ac.uk/porteous%E2%80%AFroom/ here]) on the
same floor as the main room.

== Travel ==

=== Travel to Edinburgh ===

==== Air ====

[https://www.edinburghairport.com/ Edinburgh Airport] is located
approximately 8 miles away from the city centre.

The [https://edinburghtrams.com/ Edinburgh tram] runs from the
airport every 7 minutes, the last tram from the airport leaves after
22:30 (see tram webpage).

The [https://airlink100.co.uk/ Airlink bus] (service 100) runs
between the airport and the city centre, reaching Waverley Bridge
railway station in 25 minutes. The route to and from the airport runs
24 hours a day every 10 minutes approximately during the day.

Most advance hire taxi companies will offer an airport pick-up
service. [https://www.taxis-edinburgh.co.uk/ Here's one], but any will
do. There's also a taxi hailing stand at the airport, follow the signs.

You can also fly into another main UK city and continue to Edinburgh by [[#Train|train]].

==== Train ====

Edinburgh is well-connected to most other main UK cities. There are a
few faster trains from London (about 4h25min) every day. You can use [https://www.nationalrail.co.uk/ National Rail] to plan your trip and link you to the appropriate provider.

I have enjoyed taking the Eurostar from the main continent to London. There is also the [https://www.sleeper.scot/ Caledonian Sleeper] that can get you to Edinburgh or London by 7am very slowly overnight.

=== Travel around Edinburgh ===

Edinburgh is somewhat hilly and the venue is located [https://upload.wikimedia.org/wikipedia/commons/f/ff/The_Mound%2C_Edinburgh%2C_18_September_2014.jpg up a slope].
If that is not a problem, then Edinburgh is quite walkable.

Public transportation is available. Check out [https://transportforedinburgh.com/ Transport for Edinburgh] for all the details.

* Buses. [https://www.lothianbuses.com/ Lothian buses] operates many of the relevant buses. You can pay contactless with a card or app and there's a capped pay program ('TapTapCap'). Here's the [https://www.lothianbuses.com/wp-content/uploads/2024/09/Network_Map_240908.pdf map], but I usually use Google maps for directions.

* Taxis. You can usually just hail a black cab from anywhere in the centre, see their [https://www.taxis-edinburgh.co.uk/ webpage] for advance bookings. Your favourite search engine will provide other taxi companies.

* Tram. The [https://edinburghtrams.com/ Edinburgh tram] stops fairly close to the venue, so can be an easy way to the venue.

* Uber operates in Edinburgh.

== Accommodation ==

The venue is located quite centrally, with many hotels nearby. Here are some 4-star and 3-star suggestions nearby, but you'll probably find something charming by your own (just watch out for scams). The tram and buses make it easy to also stay somewhere away from the centre and commute in if you prefer.

Hotel suggestions:
* [https://www.apexhotels.co.uk/destinations/edinburgh/apex-city-of-edinburgh-hotel/ Apex City of Edinburgh Hotel]. Main suggestion, slightly-up-and-steep-downhill from the venue. We have a 10% discount code, which I will email once I have it. '''Note:''' There is a slightly more full Apex hotel on the same street which I listed before, so if you want to be in the suggested hotel, make sure you're in the correct one.
* [https://www.motel-one.com/en/hotels/edinburgh/hotel-edinburgh-royal/ Motel One Edinburgh Royal]. A cheaper option, steep downhill from the venue.
* [https://www.scotsmanhotel.co.uk/ Scotsman Hotel]. A more expensive option, slightly-up-and-moderate-downhill from the venue.

== Weather ==

Edinburgh has temperate (and temperamental) climate, and in December it will likely be close to zero degrees centrigade, typically above. It will be windy, and potentially rainy, so make sure you dress appropriately. Locals wear waterproof/resistant clothes. Umbrellas tend to be rather useless due to the wind, one typically recognises the tourists by their futile struggles to turn inside-out umbrellas
while getting soaked.

The days are quite short in December, and you might be able to catch
the sunrise heading into the venue in the morning. I recommend
avoiding missing most of the daylight completely, e.g., make sure you go
for a short walk outside during the lunch break.

== Tourism ==

Edinburgh offers many tourist attractions and museums, and many are located centrally and close to the venue. Entrance to museums and galleries is free. Entrance to some exhibitions in the museum or gallery will require buying a separate ticket.

The meeting takes place just after [https://www.visitscotland.com/things-to-do/events/st-andrews-day Saint Andrew's Day] weekend, and Monday will be a public holiday in Scotland.
That should not affect travel, although the airport and railway might be busier than usual.

[https://www.historicenvironment.scot/about-us/news/st-andrews-day-ticket-giveaway/ Historic Environment Scotland] offer free tickets to visit some Historic Scotland attractions on Saint Andrew's day, such as the Edinburgh Castle. Registration for [https://www.historicenvironment.scot/ticket-giveaway/ free tourism tickets] opens Tuesday 12 November 10am UK time until Thursday 28 November.

If you go to the Castle, try to get there before 1pm to see them fire the Cannon.

Very near the venue is Scott Monument which you can climb, for a fee,
during the day for a stunning view. There will be a German Christmas
Market nearby I believe.

There are several hills within the city and you can easily climb up. The easiest (and closest to the venue) is [https://ewh.org.uk/calton-hill/ Calton Hill] and has a road and steps leading all the way up.

[https://www.geolsoc.org.uk/GeositesArthursSeat Arthur's Seat and the Salisbury Crags] are most visible from the centre. It takes about 1.5 hours roundtrip to get to the top. The grass can be slippery after a rain, and people can slip to their death, so wear good shoes and only climb during the day.

You can sometimes take a daytrip on a guided tour to the highlands or a whisky distillery. If you have the time, I recommend spending a few days in the former, and maybe visiting some of the latter.

I'll try to add more stuff here, especially if people send me recommendations or ask questions.

== Registration ==
Please register [https://www.epay.ed.ac.uk/conferences-and-events/college-of-science-and-engineering/school-of-informatics/informatics-events/ifip-working-group here].
After you 'Book Event', please choose either:
* '4 Day Attendee' or
* iff you're only attending partially, tick the boxes for the relevant days.

(If you plan to partially attend, please discuss with the Chairs first. I think it's somewhat unusual.)

You'll be prompted for additional details like contact details, allergies and dietary requirements after: adding to basket; proceeding to checkout; registering.

Please let me know if you have any problems. Please let me know if you won't be able to register before Thursday 28 Nov.

== Attendance ==
(Alphabetical by last name please)

* Guillaume Allais
* Nada Amin
* Sandrine Blazy
* Edwin Brady
* Jacques Carette
* Sebastian Erdweg
* Jeremy Gibbons
* Kevin Hammond
* James McKinna
* Ohad Kammar
* Paul Kelly (on 5-6 only)
* Andras Kovacs
* Lindsey Kuper
* Julia Lawall
* Ralf Lämmel
* Sam Lindley
* Peter Mosses
* Christoph Reichenbach
* Tiark Rompf
* Sven-Bodo Scholz
* Amir Shaikhha
* Friedrich Steimann
* Tijs van der Storm
* Jeremy Yallop

=== Local Observers ===
* Robert Wright

== Talks ==

See below for the schedule (but note that the actual scheduling of talks will not be available until the meeting starts). Members: please add yourself and your topic, alphabetically ordered by surname:

* Nada Amin [[WG211/M24Amin | Verified program synthesis ]]
* Sandrine Blazy [[WG211/M24Blazy | A Mechanized Semantics for Dataflow Circuits ]]
* Edwin Brady [[WG211/M24Brady | "Normalisation by Compilation": Typechecking Dependent Types via the Scheme Runtime ]]
* Jacques Carette [[WG211/M24Carette | Partial Evaluation meets Denotational Semantics ]]
* Sebastian Erdweg [[WG211/M24Erdweg | Stateful Differential Operators for Incremental Computing ]]
* Kevin Hammond [[WG211/M24Hammond | Using Formal Methods at Scale in the Delivery of a High Assurance Distributed System: the Cardano Blockchain Implementation in Haskell ]]
* Jeremy Gibbons [[WG211/M24Gibbons | Continuation−Passing Style‚ Defunctionalization‚ Accumulations‚ and Associativity ]]
* Lindsey Kuper [[WG211/M24Kuper | Library-Level Choreographic Programming ]]
* Ralf Lämmel [[WG211/M24Laemmel | Type Inference in a Knowledge-Graph Setting]]
* Peter Mosses [[ WG211/M24Mosses | Denotational Semantics in Agda ]]
* Tiark Rompf [[WG211/M24Rompf | Rhyme: A Data-Centric Multi-Paradigm Query Language ]]
* Friedrich Steimann [[ WG211/M24Steimann | A really old new metatheory of software languages ]]
* Amir Shaikhha [[ WG211M24Shaikhha | Democratizing Data Science by Leveraging Structure ]]
* Sam Lindley [[ WG211M24Lindley | Modal Effect Types ]]

We will follow our usual format of interactive talks with an active audience, using a chess clock for timing, as follows. For each talk the speaker and the audience each get at most 25 minutes. The audience does not have to wait until the end of a talk to ask questions; interaction and discussion is encouraged. (But experience from previous meetings shows that it is useful to let the speaker at least finish the introduction before interrupting.) To ensure fairness, administration of the time used by each party is done using a chess clock. Operation of the clock rotates among participants. Both speaker and audience are expected to contribute to make talks and discussions engaging, interesting, and useful. Therefore, we observe a policy of no use of electronic devices during talks (other than the device the speaker uses to present slides). Bring paper and pen for making notes.

== Program / schedule ==

=== Scientific program ===

To be determined.

Tuesday, December 3

* 8:45 - 9:00 Welcome
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Lunch
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>>

Wednesday, December 4

* 9:00 - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Lunch
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>>

Thursday, December 5

* 9:00 - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Lunch
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>>

Friday, December 6

* 9:00 - <<TBD>> <<n>> talks
** <<TBD>>-<<TBD>> <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> 1 talk
* <<TBD>> Lunch

=== Social events ===

To be determined.

WG211/M24Schedule

2024-10-04T05:02:15Z

Nada: /* Attendance */

= IFIP Working Group 2.11, Twenty-fourth Meeting =

== December 3rd (Tues) - 6th (Fri) in Edinburgh, Scotland, UK ==

The meeting will be hosted by [https://www.denotational.co.uk/ Ohad Kammar], who will write in the first person in the remainder. If you want to know anything, please email me. This page is not yet finished, I'll try to add the missing information as soon as possible.

The meeting will last 3.5 days; the first three days (Tues-Thur) will
be full-day whereas the last day (Fri) will be a half-day session.

=== Venue ===

[https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0401_01_1.07 Althaus-Reid Room, 1.07] ([http://exhibition.div.ed.ac.uk/rooms-renamed-in-honour-of-two-inspirational-female-theologians/ named after the theologian Marcella Althaus-Reid])

New College 
School of Divinity 
The University of Edinburgh 
Central Campus 
1 Mound Place 
Edinburgh EH1 2LU

This is unfortunately '''not''' the School of Informatics, which is about 15 minutes walk south from this venue.

I'll include a Google map soon with the venue, and populate it with other
relevant locations closer to the event.

==== WiFi Access ====

If you have eduroam credentials, you may use them to access the
eduroam network while at Edinburgh.

I'm looking into setting up guest accounts for participants without
eduroam credentials, and will put the information here closer to the date.

==== Workspace ====

A quiet area for shared use is available in the [https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0401_01_1.09 Porteous Room 1.09]
(you can read more about it
[https://exhibition.div.ed.ac.uk/porteous%E2%80%AFroom/ here]) on the
same floor as the main room.

== Travel ==

=== Travel to Edinburgh ===

==== Air ====

[https://www.edinburghairport.com/ Edinburgh Airport] is located
approximately 8 miles away from the city centre.

The [https://edinburghtrams.com/ Edinburgh tram] runs from the
airport every 7 minutes, the last tram from the airport leaves after
22:30 (see tram webpage).

The [https://airlink100.co.uk/ Airlink bus] (service 100) runs
between the airport and the city centre, reaching Waverley Bridge
railway station in 25 minutes. The route to and from the airport runs
24 hours a day every 10 minutes approximately during the day.

Most advance hire taxi companies will offer an airport pick-up
service. [https://www.taxis-edinburgh.co.uk/ Here's one], but any will
do. There's also a taxi hailing stand at the airport, follow the signs.

You can also fly into another main UK city and continue to Edinburgh by [[#Train|train]].

==== Train ====

Edinburgh is well-connected to most other main UK cities. There are a
few faster trains from London (about 4h25min) every day. You can use [https://www.nationalrail.co.uk/ National Rail] to plan your trip and link you to the appropriate provider.

I have enjoyed taking the Eurostar from the main continent to London. There is also the [https://www.sleeper.scot/ Caledonian Sleeper] that can get you to Edinburgh or London by 7am very slowly overnight.

=== Travel around Edinburgh ===

Edinburgh is somewhat hilly and the venue is located [https://upload.wikimedia.org/wikipedia/commons/f/ff/The_Mound%2C_Edinburgh%2C_18_September_2014.jpg up a slope].
If that is not a problem, then Edinburgh is quite walkable.

Public transportation is available. Check out [https://transportforedinburgh.com/ Transport for Edinburgh] for all the details.

* Buses. [https://www.lothianbuses.com/ Lothian buses] operates many of the relevant buses. You can pay contactless with a card or app and there's a capped pay program ('TapTapCap'). Here's the [https://www.lothianbuses.com/wp-content/uploads/2024/09/Network_Map_240908.pdf map], but I usually use Google maps for directions.

* Taxis. You can usually just hail a black cab from anywhere in the centre, see their [https://www.taxis-edinburgh.co.uk/ webpage] for advance bookings. Your favourite search engine will provide other taxi companies.

* Tram. The [https://edinburghtrams.com/ Edinburgh tram] stops fairly close to the venue, so can be an easy way to the venue.

* Uber operates in Edinburgh.

== Accommodation ==

The venue is located quite centrally, with many hotels nearby. I'll
filter out some 3-star and 4-star suggestions nearby soon, but you'll
probably find somewhere charming by your own (just watch out for scams).
The tram and buses make it easy to also stay somewhere away from the
centre and commute in if you prefer.

== Weather ==

Edinburgh has temperate (and temperamental) climate, and in December it will likely be close to zero degrees centrigade, typically above. It will be windy, and potentially rainy, so make sure you dress appropriately. Locals wear waterproof/resistant clothes. Umbrellas tend to be rather useless due to the wind, one typically recognises the tourists by their futile struggles to turn inside-out umbrellas
while getting soaked.

The days are quite short in December, and you might be able to catch
the sunrise heading into the venue in the morning. I recommend
avoiding missing most of the daylight completely, e.g., make sure you go
for a short walk outside during the lunch break.

== Tourism ==

Edinburgh offers many tourist attractions and museums, and many are located centrally and close to the venue. Entrance to museums and galleries is free. Entrance to some exhibitions in the museum or gallery will require buying a separate ticket.

The meeting takes place just after [https://www.visitscotland.com/things-to-do/events/st-andrews-day Saint Andrew's Day] weekend, and Monday will be a public holiday in Scotland.
That should not affect travel, although the airport and railway might be busier than usual.

[https://www.historicenvironment.scot/about-us/news/st-andrews-day-ticket-giveaway/ Historic Environment Scotland] offer free tickets to visit some Historic Scotland attractions on Saint Andrew's day, such as the Edinburgh Castle. Registration for [https://www.historicenvironment.scot/ticket-giveaway/ free tourism tickets] opens Tuesday 12 November 10am UK time until Thursday 28 November.

If you go to the Castle, try to get there before 1pm to see them fire the Cannon.

Very near the venue is Scott Monument which you can climb, for a fee,
during the day for a stunning view. There will be a German Christmas
Market nearby I believe.

There are several hills within the city and you can easily climb up. The easiest (and closest to the venue) is [https://ewh.org.uk/calton-hill/ Carlton Hill] and has a road and steps leading all the way up.

[https://www.geolsoc.org.uk/GeositesArthursSeat Arthur's Seat and the Salisbury Crags] are most visible from the centre. It takes about 1.5 hours roundtrip to get to the top. The grass can be slippery after a rain, and people can slip to their death, so wear good shoes and only climb during the day.

You can sometimes take a daytrip on a guided tour to the highlands or a whisky distillery. If you have the time, I recommend spending a few days in the former, and maybe visiting some of the latter.

I'll try to add more stuff here, especially if people send me recommendations or ask questions.

== Registration ==

Working on it, I'll put up more details soon.

== Attendance ==
(Alphabetical by last name please)

* Guillaume Allais
* Nada Amin
* Edwin Brady
* Jacques Carette
* Sebastian Erdweg
* Ohad Kammar
* Andras Kovacs
* Lindsey Kuper
* Julia Lawall
* Peter Mosses
* Christoph Reichenbach
* Tiark Rompf
* Sven-Bodo Scholz
* Tijs van der Storm
* Jeremy Yallop

=== Local Observers ===

== Talks ==

See below for the schedule (but note that the actual scheduling of talks will not be available until the meeting starts). Members: please add yourself and your topic, alphabetically ordered by surname:

* Edwin Brady [[WG211/M24Brady | "Normalisation by Compilation": Typechecking Dependent Types via the Scheme Runtime ]]
* Tiark Rompf [[WG211/M24Rompf | Rhyme: A Data-Centric Multi-Paradigm Query Language ]]

We will follow our usual format of interactive talks with an active audience, using a chess clock for timing, as follows. For each talk the speaker and the audience each get at most 25 minutes. The audience does not have to wait until the end of a talk to ask questions; interaction and discussion is encouraged. (But experience from previous meetings shows that it is useful to let the speaker at least finish the introduction before interrupting.) To ensure fairness, administration of the time used by each party is done using a chess clock. Operation of the clock rotates among participants. Both speaker and audience are expected to contribute to make talks and discussions engaging, interesting, and useful. Therefore, we observe a policy of no use of electronic devices during talks (other than the device the speaker uses to present slides). Bring paper and pen for making notes.

== Program / schedule ==

=== Scientific program ===

To be determined.

Tuesday, December 3

* 8:45 - 9:00 Welcome
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Lunch
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>>

Wednesday, December 4

* 9:00 - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Lunch
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>>

Thursday, December 5

* 9:00 - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>> Lunch
* <<TBD>> - <<TBD>> <n> talks
** <<TBD>> - <<TBD>>
* <<TBD>> - <<TBD>>

Friday, December 6

* 9:00 - <<TBD>> <<n>> talks
** <<TBD>>-<<TBD>> <<TBD>>
* <<TBD>> - <<TBD>> Break
* <<TBD>> - <<TBD>> 1 talk
* <<TBD>> Lunch

=== Social events ===

To be determined.

WG211/M23Amin

2024-03-10T23:55:54Z

Nada:

In [[WG211/M21Amin | Odense]], I (Nada Amin) presented staged-miniKanren, which augments miniKanren (a relational programming language) with staging constructs. Since then, we (Michael Ballantyne, Raffi Sanna, Will Byrd and Nada Amin) have added support for novel features to account for non-determinism and stage polymorphism. We use staged-miniKanren to stage interpreters written as relations, in which the programs under interpretation are allowed to contain holes representing unknown values. We apply this staging framework to a relational interpreter for a subset of Racket, and demonstrate significant performance gains across multiple synthesis problems.

WG211/M23Amin

2024-03-10T23:53:35Z

Nada: Created page with "In Odense, I (Nada Amin) presented staged-miniKanren, which augments miniKanren (a relational programming language) with staging constructs. Since then, we (Michael Ballantyne..."

In Odense, I (Nada Amin) presented staged-miniKanren, which augments miniKanren (a relational programming language) with staging constructs. Since then, we (Michael Ballantyne, Raffi Sanna, Will Byrd and Nada Amin) have added support for novel features to account for non-determinism and stage polymorphism. We use staged-miniKanren to stage interpreters written as relations, in which the programs under interpretation are allowed to contain holes representing unknown values. We apply this staging framework to a relational interpreter for a subset of Racket, and demonstrate significant performance gains across multiple synthesis problems.

WG211/M23Schedule

2024-03-10T23:52:57Z

Nada: /* Talks */

= IFIP Working Group 2.11, Twenty-third Meeting =

== March 25th–28th 2024 in Philadelphia, Pennsylvania, USA ==

The meeting will be hosted by [https://www.cs.drexel.edu/~gbm26/ Geoffrey Mainland].

The meeting will last 3.5 days; the first three days will be full-day, whereas the last day will be a half-day session.

=== Venue ===

[https://drexel.edu/cci/ Drexel College of Computing and Informatics] 
[https://ucitysquare.com/property/3675-market-street/ 3675 Market Street]

=== Travel ===

Philadelphia International Airport (PHL) has frequent flights to both Europe and the USA/Canada. A taxi between PHL and the Center City Zone of Philadelphia, which includes the venue and most hotels, costs a flat rate of $32.00. There is a taxi queue. Uber and Lyft have designated pick-up and drop-off areas at the airport; they are sometimes less expensive and sometimes more expensive than a taxi. It is possible to take regional rail to University City (Penn Medicine Station) and walk/take a car from there, but that is much less convenient.

It is also possible to fly into Newark Liberty International Airport (EWR) and take Amtrak from there to 30th St. Station. The trip takes slightly over an hour, and train ticket prices vary widely depending on time of day and how far one books in advance ($20-$100 each way). 30th St. Station is a 15-20 minute walk from the venue (a straight shot down Market St.).

Amtrak also provides reliable, regular service to New York City (about 1.5 hours) and Washington D.C. (about 2 hours). If you are extending your stay and would like to visit either of these cities, that could be a viable option. It might make sense to fly into New York City just for the meeting, but flying in to D.C. would not be a good choice. Email Geoff if you're thinking about either option.

==== Getting Around Philadelphia ====

Philadelphia is a very walkable city. It is both pedestrian and bicycle friendly, with designated bike lanes on many streets. SEPTA provides metro (reliable) and bus (not so reliable) service throughout the city. I (Geoff) usually walk everywhere, including between work and home (about 1.5 miles/2.4 km). Center City and University City (where the venue is) are quite safe. There is a SEPTA trolley stop a block away from the venue.

==== Philadelphia Transportation Resources ====

* [https://philapark.org/taxicab-tariffs/ Taxi tariffs]
* [https://www.septa.org/schedules/AIR Regional rail from PHL]
* [https://www.amtrak.com/ Amtrak]
* [https://www.rideindego.com/ Indego] city bikes
* [https://www.septa.org/ SEPTA] Metro, bus, and regional rail.

=== Accommodation ===

We have negotiated a rate of $159/night for a block of 25 rooms at the Sheraton University City, which is the closest hotel to the venue. To receive this rate, we must guarantee 80% occupancy, so please book at the Sheraton if you can.

You may book a room at [https://www.marriott.com/event-reservations/reservation-link.mi?id=1707507388612&key=GRP&app=resvlink this direct link] or by calling +1 888 627 7071. '''The deadline for reservations is Thursday, February 29'''.

=== Registration ===

Registration is available at [https://secure.touchnet.com/C20688_ustores/web/product_detail.jsp?PRODUCTID=4416&SINGLESTORE=true this link]. The registration fee covers:

* Coffee and group lunches for all 4 days.
* The group excursion to the [https://www.barnesfoundation.org/ Barnes Foundation] Monday afternoon.
* A group dinner on Tuesday.

== Attendance ==
(Alphabetical by last name please)

* Nada Amin
* Michael Ballantyne
* Jacques Carette
* Colin Gordon
* Jeremy Johnson
* Yukiyoshi Kameyama
* Ohad Kammar
* Martin Kellog
* Oleg Kiselyov
* András Kovács
* Julia Lawall
* Geoffrey Mainland
* Igor Pikovets
* Sven-Bodo Scholz
* Ken Shan
* Satnam Singh
* Friedrich Steimann
* Stephanie Weirich
* Eric Van Wyk
* Jeremy Yallop

== Talks ==

See below for the schedule (but note that the actual scheduling of talks will not be available until the meeting starts). Members: please add yourself and your topic, alphabetically ordered by surname:

* Nada Amin [[WG211/M23Amin | A Redesign for Staged Relational Programming ]]
* Jacques Carette [[WG211/M23Carette | Partial Evaluation meets Denotational Semantics ]]
* Julia Lawall [[WG211/M23Lawall | Towards Verification of Linux Kernel Code]]
* Satnam Singh [[WG211/M23Singh | Haste: A Haskell DSL for Programming the Groq TSP/LPU Machine Learning Chips ]]

We will follow our usual format of interactive talks with an active audience, using a chess clock for timing, as follows. For each talk the speaker and the audience each get at most 25 minutes. The audience does not have to wait until the end of a talk to ask questions; interaction and discussion is encouraged. (But experience from previous meetings shows that it is useful to let the speaker at least finish the introduction before interrupting.) To ensure fairness, administration of the time used by each party is done using a chess clock. Operation of the clock rotates among participants. Both speaker and audience are expected to contribute to make talks and discussions engaging, interesting, and useful. Therefore, we observe a policy of no use of electronic devices during talks (other than the device the speaker uses to present slides). Bring paper and pen for making notes.

== Program / schedule ==

TBA

=== Social events ===

An excursion has been arranged for Monday afternoon and a group dinner will take place Tuesday evening.