[TYPES/announce] Sam Staton giving this year's LMS/BCS-FACS Evening Seminar (online) -- registration open until this Wednesday at 5PM, UTC

[Andrei Popescu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

EVENT: Annual LMS/BCS-FACS Evening Seminar

SPEAKER: Sam Staton, University of Oxford
TITLE: Programming-based foundations for statistics

DATE: Thursday, 17 November 2022, Starting time: 18:00 UTC
VENUE: Online via Zoom
EVENT PAGE: 
https://urldefense.com/v3/__https://www.lms.ac.uk/events/lectures/lms-bcs-facs-evening-seminars__;!!IBzWLUs!XSgrIhXR1p1jOKG1y5-RK0Su79NZHATVtJ-o2Dn7hrPV8DnZpuVuU4EgPlIsnkoq1P_JuO0t9vWL5xyrV87D70LbAk4cnbIf-q9OmkmV$
 
REGISTRATION LINK: 
https://urldefense.com/v3/__https://www.lms.ac.uk/civicrm/event/register?id=88=1__;!!IBzWLUs!XSgrIhXR1p1jOKG1y5-RK0Su79NZHATVtJ-o2Dn7hrPV8DnZpuVuU4EgPlIsnkoq1P_JuO0t9vWL5xyrV87D70LbAk4cnbIf-vFm4sOV$
 

Prior registration is required for attendance -- the registration site
will close on Wednesday, 16 November, at 17:00

SYNOPSIS

Probabilistic programming is a popular tool for statistics and
machine learning. The idea is to describe a statistical model as
a program with random choices. The program might be a simulation
of a system, such as a physics model, a model of viral spread,
or a model of electoral behaviour. We can now carry out
statistical inference over the system, for example, by running a
Monte Carlo simulation – running the simulation 100,000’s of
times.

As I will discuss in this talk, the idea of treating statistical
models as computer programs also has a foundational appeal. If
we can understand statistical models as programs, then the
foundations of probability and statistics can be discussed in
terms of program semantics. There is a chance of new
foundational perspectives on statistics, in terms of programming
languages and their formal methods.

As I will explain, this programming-based foundation for
statistics is attractive because there are some intuitively
simple scenarios, such as inference over function spaces, which
have an easy programming implementation, but for which the
traditional mathematical interpretation is complicated.

SPEAKER BIOGRAPHY

Sam Staton is a Professor of Computer Science and Royal Society
University Research Fellow at the University of Oxford. There he
currently runs an ERC grant "Better Languages for Statistics".
Before arriving in Oxford in 2015, Sam spent time in Nijmegen,
Paris, and Cambridge. His PhD was in Cambridge with Marcelo
Fiore (2007). Sam's main research is in programming language
theory, but he is also interested in logic and category theory.
He has recent contributions in probabilistic programming
languages, and quantum computing and programming languages.

Webpage: 
https://urldefense.com/v3/__https://www.cs.ox.ac.uk/people/samuel.staton/main.html__;!!IBzWLUs!XSgrIhXR1p1jOKG1y5-RK0Su79NZHATVtJ-o2Dn7hrPV8DnZpuVuU4EgPlIsnkoq1P_JuO0t9vWL5xyrV87D70LbAk4cnbIf-pNv5HnP$
 

[TYPES/announce] ANU Logic Summer School: Call for Participation

[Dirk Pattinson]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear Colleagues,

after last year's online edition of the logic summer school,  it is our 
greatest pleasure to announce
that we organise

  The Logic Summer School @ ANU
   5-16 December 2022
  as an in-person event


Programme and registration form at

  
https://urldefense.com/v3/__http://lss.cecs.anu.edu.au__;!!IBzWLUs!XI6JHNHwsuHTghUFg-PRklcn4O_2ejcVTEBO-mwkkgqO9XRPNKLzXNBavYcPXlNw5lElX0jTuzZ9aFDJyLR24zJRSg4JtyUh9SqpnEgHig$
  



with registration opening later today.  Everybody is most welcome.

Please consider to attend yourself, and please spread the word to your 
undergrads, your PhD students,your PostDocs, and your colleagues!


Yours with best wishes,

Peter Hoefner, Dirk Pattinson
Organisers, ANU Logic Summer School

[TYPES/announce] ProofGeneal release 4.5

[pierre . courtieu]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear list,
We are happy to announce the release of [Proof General version 
4.5](https://urldefense.com/v3/__https://github.com/ProofGeneral/PG/releases/tag/v4.5__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDhL2n9kFg$
 ).

Proof General is a generic Emacs mode for proof assistants. It can be 
instantiated for the proof assistant of your choice, and is supplied 
ready-customized for Coq, PhoX, EasyCrypt, Qrhl-tool.

Website: 
https://urldefense.com/v3/__https://proofgeneral.github.io/__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDgZe5gBLA$
 
Core maintainers e-mail: proof-general-maintain...@groupes.renater.fr

Proof General includes these features, amongst others:

- Script management: proof assistant state reflected in editor
- Commands for building and replaying proofs
- Syntax highlighting of proof scripts and prover output; hiding proofs
- Menu for jumping to theorems in a proof script
- Provision to easily run proof assistant on a remote host
- Works on any system where emacs and coq are running

## Summary of changes from 4.4 to 4.5:

### Generic changes

- **proof-general** is now a MELPA 
(https://urldefense.com/v3/__https://melpa.org/*/proof-general__;Iw!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDjngAIi6g$
 ) and NonGNU ELPA 
(https://urldefense.com/v3/__https://elpa.nongnu.org/nongnu-devel/proof-general.html__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDgsR7a85Q$
 ) Emacs package.
- It now requires GNU Emacs 25.2 or later
- License changed to GPL-3.0-or-later
- Remove support for the following systems:
 Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.
- Support for Qrhl-tool (by Dominique Unruh)
- Support for EasyCrypt (by Pierre-Yves Strub)
- PG's manual is continuously deployed at 
https://urldefense.com/v3/__https://proofgeneral.github.io/doc/master/userman/__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDghKm3sRw$
 

### Coq changes

- Auto Compilation of Requires improved:
 - support of vos/vok compilation
 - background compilation
- "Omit complete opaque proofs" mode for speed.
- Automatic insertion of "Proof using" annotations.
- Folding/unfolding hypotheses.
- Support Ssreflect's `move=>` intro style with `C-c C-a TAB`
- Support Coq's ``Diffs`` and ``Show Proof Diffs`` features.

### Miscellaneous

- New mode: `opam-switch-mode` 
(https://urldefense.com/v3/__https://github.com/ProofGeneral/opam-switch-mode__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDiHZBvpkg$
 ), also distributed on MELPA, allows to easily perform `opam switch` (and thus 
switch between coq versions) from within Emacs.
- To keep PG up-to-date 
(https://urldefense.com/v3/__https://proofgeneral.github.io/*keeping-proof-general-up-to-date__;Iw!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDgzWE0gLQ$
 ), we recommend to install PG from MELPA or NonGNU-devel-ELPA and use `M-x 
proof-upgrade-elpa-packages RET` every once in a while.

The ProofGeneral Team

[TYPES/announce] Assistant professor position in Theoretical Computer Science at University of Groningen.

[Jorge A . Pérez]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear colleagues,

The University of Groningen (NL) invites applications for one
assistant professor position (tenure-track) in Theoretical Computer
Science.

The successful candidate will join us at the Fundamental Computing
group of the Bernoulli Institute for Mathematics, Computer Science and
AI.
The group already has research expertise on concurrency theory, modal
logic, coalgebra, and proof theory (see 
https://urldefense.com/v3/__http://www.rug.nl/fse/fc__;!!IBzWLUs!QOUjCGWM_sgjWSvO9yEQkjwqv94X0927WoHU5V89MVYusZnnsomN-pHOPisHrDG54uAmyf1-a5H5M5_pw75GZYUkotQu48DH$
 ); we
seek to reinforce our profile in Theoretical Computer Science, very
broadly construed.

This is a tenure-track position with 60% teaching - 30% research - 10%
organizational tasks.
Our tenure-track system offers well-defined perspectives for career
and personal development.
In particular, after five years of appointment, assistant professors
are assessed for tenure and promotion to associate professor.

The application deadline is January 8, 2023.
For further details about this position, our tenure-track system, and
the link to the application form see
https://urldefense.com/v3/__https://www.rug.nl/about-ug/work-with-us/job-opportunities/?details=00347-02S0009PCP=wp__;!!IBzWLUs!QOUjCGWM_sgjWSvO9yEQkjwqv94X0927WoHU5V89MVYusZnnsomN-pHOPisHrDG54uAmyf1-a5H5M5_pw75GZYUkoo0MByUP$
 
.

Please disseminate widely among potential candidates. If you have any
questions, please feel free to contact me .

Best wishes,
Jorge

--
Jorge A. Pérez
Associate Professor
Leader, Fundamental Computing group
Bernoulli Institute for Math, CS and AI
University of Groningen, The Netherlands
  /  

[TYPES/announce] PhD positions in Blockchain and DLT including analysis and verification of smart contracts using Horn clauses

[Fabio Fioravanti]

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are looking for strong and motivated candidates for 11 PhD positions in the 
Italian National PhD Program in Blockchain and and Distributed Ledger 
Technology at various Italian universities.

Application deadline:  18 november 2022
Interviews: 21-24 november 2022
PhD Program website: https://urldefense.com/v3/__https://isas.unicam.it/dni/blockchain-and-DLT__;!!IBzWLUs!QCuxq6pIUrFazTXZx_MMGyaUIESm0PqDGht59-uQ55ZAFGQd7Yh-WPsSr30951Rvw1aNPkopI2eejhBlcAKbZ1Wzz5aXKha6rSM$  
Application details and research topics:  https://urldefense.com/v3/__https://www.unicam.it/bandi/bando-n-76799-del-07112022__;!!IBzWLUs!QCuxq6pIUrFazTXZx_MMGyaUIESm0PqDGht59-uQ55ZAFGQd7Yh-WPsSr30951Rvw1aNPkopI2eejhBlcAKbZ1Wzz5aXjTFQhyU$  



In particular, one position is on analysis, verification and testing of smart 
contracts using constrained Horn clauses (CHC) at the University of 
Chieti-Pescara.
For further information please contact Fabio Fioravanti 
fabio.fiorava...@unich.it

Best regards


--
Fabio Fioravanti
University of Chieti-Pescara, Italy
fabio.fiorava...@unich.it
https://urldefense.com/v3/__https://www.sci.unich.it/*fioravan/__;fg!!IBzWLUs!QCuxq6pIUrFazTXZx_MMGyaUIESm0PqDGht59-uQ55ZAFGQd7Yh-WPsSr30951Rvw1aNPkopI2eejhBlcAKbZ1Wzz5aXl-0hCBA$  

[TYPES/announce] Postdoc Position on Hardware Verification via Model Learning, Royal Holloway University of London -- Application deadline 7 Dec 2022

[Sammartino, Matteo]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

- Application deadline: Midnight, 7 Dec 2022
- Salary: £37,467
- Duration: until November 2023

Applications are invited for the post of Post-Doctoral Research Assistant in 
the Computer Science Department at Royal Holloway, University of London.

The post holder will have an exciting opportunity to work on the EPSRC-funded 
"Verification of Hardware Concurrency via Model Learning" (CLeVer) project
(EP/S028641/1), led by Prof. Alexandra Silva (UCL/Cornell) and Matteo 
Sammartino (RHUL), in collaboration with ARM, world-leading designer of 
multi-core chips.

For an informal discussion about the post, please contact Dr. Matteo Sammartino 
on matteo.sammart...@rhul.ac.uk.

# Brief description of the project

Digital devices are increasingly complex, therefore there is a pressing need to 
automate the assessment of their correctness. Formal verification provides 
highly effective techniques to assess the correctness of systems. However, 
formal models are usually built by humans, and as such can be error-prone and 
inaccurate.

The project aims to develop a novel verification framework for hardware, which 
combines learning, testing and model-checking. Not all models are suitable for 
this purpose and hence specific classes of models will need to be developed, 
depending on the task at hand. Subsequently, learning and verification 
techniques for these classes need to be devised and tested in realistic case 
studies. We have an industrial partner, ARM, that will provide valuable 
guidance on the design and development of the aforementioned tasks.

# The ideal candidate

We are looking for candidates with a PhD in one of the following areas: 
model-based testing and verification, model learning, automated analysis of 
hardware systems. Experience in multiple areas will be valued. Candidates 
ideally should also have strong programming skills.

# Where to apply

https://urldefense.com/v3/__https://jobs.royalholloway.ac.uk/0922-411-R__;!!IBzWLUs!Ql4x98AHBGBXp8EftOjO8vr9oTKppmjfsdYpqCJyeLkaUYZbajCRXcVw1LdY-wgIUroTgr7fZ4Oeq9LVpCtQ5NwmmyKAU69TUSdFpOq5C3-D$
  


Best wishes,

   Matteo Sammartino


==
Matteo Sammartino, Lecturer
Royal Holloway University of London
Department of Computer Science
Tel.: (+44) (0) 1784 44 3690
Office: 2-07, Bedford Building
https://urldefense.com/v3/__https://matteosammartino.com/__;!!IBzWLUs!Ql4x98AHBGBXp8EftOjO8vr9oTKppmjfsdYpqCJyeLkaUYZbajCRXcVw1LdY-wgIUroTgr7fZ4Oeq9LVpCtQ5NwmmyKAU69TUSdFpA87nBfj$
  


This email, its contents and any attachments are intended solely for the 
addressee and may contain confidential information. In certain circumstances, 
it may also be subject to legal privilege. Any unauthorised use, disclosure, or 
copying is not permitted. If you have received this email in error, please 
notify us and immediately and permanently delete it. Any views or opinions 
expressed in personal emails are solely those of the author and do not 
necessarily represent those of Royal Holloway, University of London. It is your 
responsibility to ensure that this email and any attachments are virus free.

[TYPES/announce] CONFEST 2023 -- Call for Workshop Proposals

[Emmanuel Filiot]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

* CONFEST 2023 * -- Call for Workshop Proposals

September 18 - September 23 2023, Antwerpen, Belgium

(https://urldefense.com/v3/__https://www.uantwerpen.be/en/conferences/confest-2023/__;!!IBzWLUs!UDhIR1yBiG58TiSgD_ZGygASRynK_B798rd_ExCFciq4FvKEMoDic4oVO5LDy9lhtrzhwCQD5WJ3wwJXR_-P23ZSzT3oOA$
  

)

CONFEST is an umbrella conference comprising four international meetings:



- CONCUR (34th International Conference on Concurrency Theory),

- QEST (20th International Conference on Quantitative Evaluation of
SysTems),

- FORMATS (21st International Conference on Formal Modeling and Analysis of
Timed Systems), and

- FMICS (28th International Conference on Formal Methods for Industrial
Critical Systems).


Researchers and practitioners are invited to submit proposals for ONE DAY

workshops on topics related to theory, formal modeling, verification,
performance evaluation and engineering of concurrent, timed, industrial,
and other systems.

Typically, CONFEST workshops feature a number of invited speakers and a
number of contributed presentations.

The workshops will take place one day before (18 September) and one day
after (23 September) the main conferences.


TOPICS


The purpose of the workshops is to provide participants with a friendly,
stimulating, and interactive atmosphere for

- presenting novel ideas,

- discussing their applications,

- encouraging cross-fertilization between industry and academia, and

- fostering opportunities for young and prospective researchers.

ORGANIZATION

CONFEST’23 is planned as a physical, in-person event, with some support for
remote participation.

In a limited number of cases, there will be remote-participation support
for speakers and for other

participants who are unable to come. Please take this into account when
preparing a workshop

proposal and communicate to participants requiring such support that they
should contact the

organisers of CONFEST explaining their case.



We will provide the following to workshop organisers:


- Meeting rooms on demand


- Coffee breaks, catering for lunch, both are included


- CONFEST'23 website cannot be made accessible for edits by third parties

but workshop organisers can either host their own website and provide a
link to it

that we put on CONFEST website, or they send us their content and we put it
in the website.


- Registration will be centralized by CONFEST.


- Special rates for hotels, which can be found in the website
https://urldefense.com/v3/__https://www.uantwerpen.be/en/conferences/confest-2023/info/__;!!IBzWLUs!UDhIR1yBiG58TiSgD_ZGygASRynK_B798rd_ExCFciq4FvKEMoDic4oVO5LDy9lhtrzhwCQD5WJ3wwJXR_-P23ZAY-qe-g$
  

,

as well as further local information about Antwerp.


INSTRUCTIONS FOR PROPOSAL SUBMISSION


Workshop proposals should include:


-  The name and the preferred date of the proposed workshop.



-  The names and contact information (web page, email address) of the
organisers.

-  A short scientific summary and justification of the proposed topic for
the CONFEST community (500 words max).

-  A discussion of the proposed format and agenda.

-  If applicable, a brief description of past versions of the workshop,
including
dates, organisers, submission and acceptance counts, and attendance.

-  Procedures for selecting papers and participants.

-  The publication plan (only invited speakers, no published proceedings,
pre-/post-proceedings published with EPTCS/ENTCS/...).

-  Potentially invited speakers.

-  Tentative schedule for paper submission and notification of acceptance.

The main responsibility for organizing the workshop goes to the workshop
organiser(s), including:

- workshop publicity (possibly including call for papers, submission and
review process)

- scheduling of workshop activities in collaboration with the CONFEST
workshop chair.



Proposals should be sent to Emmanuel Filiot (workshop chair):


efil...@gmail.com

IMPORTANT DATES

  - Submission deadline February 2, 2023

  - Notification February 16, 2023

  - Program of the workshops ready: August 16, 2023


  - Workshops: September 18, 23, 2023