[TYPES/announce] Agda Implementors' Meeting XXXI - Edinburgh, 1-7 April 2020

[Wen Kokke]

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

---
Agda Implementors' Meeting XXXI
Call for participation
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXXI 

---

The thirty-first Agda Implementors' Meeting will take place in Edinburgh, 
Scotland from Wednesday 1 April 2020 to Tuesday 7 April 2020. The meeting will 
be similar to previous ones:

* Presentations concerning theory, implementation, and use cases of 
Agda and other Agda-like languages.
* Discussions around issues related to the Agda language.
* Plenty of time to work in, on, under or around Agda, in collaboration 
with other participants.

To register for AIM XXXI, please fill out the form below and send it to Wen 
Kokke mailto:wen.ko...@ed.ac.uk>>

Preliminary information (more appearing later) is available at:
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXXI 


I hope to see you there!

Kind regards,
Wen

---
Registration form for Agda Implementors' Meeting XXXI

Name:

Title and optionally abstract (if you want to give a talk or lead a discussion):

Suggestions for code sprints (optional):

Additional comments:
---

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[TYPES/announce] Postdoctoral position in FAU Erlangen-Nürnberg

[Sergey Goncharov]

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


[We would be grateful for further distribution of the job advertisement
below]

In the Theoretical Computer Science group (Chair Computer Science 8) at
the Friedrich-Alexander-Universität Erlangen-Nürnberg, we have a
*one-year* postdoc position available in the DFG-Project "A High Level
Language for Programming and Specifying Multi-Effect Algorithms", which
is concerned with monad-based semantics and program logics for
side-effecting (guarded) iteration and recursion. The technical part of
the project proposal can be made available on request.

The project is supervised by Sergey Goncharov and Lutz Schröder. The
positions are in the TV-L E13 or E14 pay scale depending on
qualification of the applicant. The position is available immediately
but can also be filled later.

Please enquire or apply by e-mail to

   {sergey.goncharov,lutz.schroeder}@fau.de

Best,

Sergey and Lutz






smime.p7s
Description: S/MIME Cryptographic Signature

[TYPES/announce] PhD Position in in Theory and Implementation of Dependently Typed Programming Languages

[Jesper Cockx]

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

Hello all,

I'm very excited to announce that I'm hiring a PhD student to work with me
at TU Delft on the theory and implementation of Agda and similar
dependently typed programming languages. If you are (know someone who could
be) interested, you can find more information about the application process
at http://pl.ewi.tudelft.nl/hiring/2020-phd-student-dependent-types/.

Best regards,
Jesper Cockx

[TYPES/announce] Final CfP: Workshop "Proofs, Computation and Meaning"

[Paolo Pistone]

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

*Apologies for cross postings*

***
Final CfP: Workshop "Proofs, Computation and Meaning"

University of Tübingen (Germany), 20-21 March 2020

http://ls.informatik.uni-tuebingen.de/PCM/

***

SCOPE:

Around thirty years after the fall of Hilbert's program, the proofs-as-programs 
paradigm established the view that a proof should not be identified, as in 
Hilbert's metamathematics, with a string of symbols in some formal system. 
Rather, proofs should consist in computational or epistemic objects conveying 
evidence to mathematical propositions. The relationship between formal 
derivations and proofs should then be analogous to the one between words and 
their meanings.


This view naturally gives rise to questions such as “which conditions should a 
formal arrangement of symbols satisfy to represent a proof?” or “when do two 
formal derivations represent the same proof?". These questions underlie past 
and current research in proof theory both in the theoretical computer science 
community (e.g. categorical logic, domain theory, linear logic) and in the 
philosophy community (e.g. proof-theoretic semantics).

In spite of these common motivations and historical roots, it seems that today 
proof theorists in philosophy and in computer science are losing sight of each 
other. This workshop aims at contributing to a renaissance of the interaction 
between researchers with different backgrounds by establishing a constructive 
environment for exchanging views, problems and results.


***

IMPORTANT DATES:

Extended abstract submission deadline: 15 January 2020
Student grant application deadline: 15 January 2020
Notification: 25 January 2020

Workshop: 20-21 March 2020
Warm-up for Master and PhD students: 19 March 2020


***

INVITED SPEAKERS:

In addition to regular invited talks, the workshop includes two tutorials, 
aimed at introducing recent ideas on the correspondence between proofs, 
programs and categories as well as to the historical and philosophical aspects 
of the notions of infinity and predicativity.

Tutorials:

- Laura Crosilla (University of Oslo)
- Noam Zeilberger (University of Birmingham)

Regular speakers:

- Bahareh Afshari (University of Gothenburg)
- Federico Aschieri (TU Vienna)
- Gilda Ferreira (Universidade Aberta, University of Lisbon)
- Dominic Hughes (UC Berkeley)
- Alberto Naibo (Paris 1 University)
- Gabriel Scherer (INRIA, Saclay)


***

SUBMISSIONS:

We invite submissions for contributed talks on topics related to the themes of 
the meeting. These include, but are not restricted to:

- Identity of proofs
- Graphical/diagrammatic representations of proofs
- Typed vs untyped proof theory
- Paradoxes and circular reasoning
- Constructivism and (im)predicativity
- Duality proofs/refutations
- Computational interpretations of classical and non-classical logics
- Non-deterministic/probabilistic aspects of computation
- Inductive/co-inductive constructions in proof theory and type theory
- (Higher-)categorical proof theory
- Substructural aspects of logic
- Philosophical and historical reflections on any of the above

Submissions should consist in a 1-2 pages extended abstract and should be sent 
to luca.tranch...@gmail.com or paolo.pist...@uniroma3.it by 15 JANUARY 2020.


***

CALL FOR PARTICIPATION AND TRAVEL GRANTS:

If you wish to attend without giving a talk, please send an e-mail to 
luca.tranch...@gmail.com or paolo.pist...@uniroma3.it.

To encourage the participation of Master and PhD students we offer a limited 
number of travel grants.

Moreover, a warm-up introducing the proofs-as-programs correspondence between 
proof theory and type theory will be organized on 19 March the day before the 
start of the workshop. (The warm-up will consists in two 2-hours lectures by 
the organizers).

Finally, there might be possibility to get ECTS credits for PhD students 
attending the workshop.

Travel grant applications must include a 1-page motivation letter and a cv and 
must be sent to luca.tranch...@gmail.com or paolo.pist...@uniroma3.it by 15 
JANUARY 2020.


***

REGISTRATION:

There will be a small registration fee (20 euros) covering both coffee breaks 
and the social dinner to be paid on arrival.


***

ORGANIZERS:

Luca Tranchini (Tübingen University), 

[TYPES/announce] EXTENDED DEADLINE for CFP ARITH-2020, IEEE Symposium on Computer Arithmetic, June 7-10, Portland, OR, USA

[Arnaud Tisserand]

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

Our apologies for multiple emails on this CFP.

The deadlines have been extended for additional weeks (see dates below).

--
 CALL FOR PAPERS
   ARITH-2020
27th IEEE Symposium on Computer Arithmetic
   June 7 - 10, 2020, Portland, OR, USA
  http://www.arithsymposium.org

--

=== Scope 

Since 1969, the ARITH symposia have served as the flagship conference for 
presenting scientific work on the latest research in computer arithmetic. 
Computer arithmetic is now driving the most important innovations and product 
directions in our industry, such as artificial intelligence and security.

Authors are invited to submit papers describing recent advances on all aspects
related to computer arithmetic, its applications or implementations. This 
includes, but is not restricted to, the following topics:

 * Foundations of number systems and arithmetic
 * Arithmetic processor design and implementation
 * Arithmetic algorithms and their analysis
 * Floating-point units, algorithms, and numerical analysis
 * Elementary and special function implementations
 * Test, validation, and formal verification techniques for arithmetic 
implementations
 * Power-efficient or low-energy arithmetic units and processors
 * Industrial implementation of arithmetic units and processors
 * Fault/error-tolerance in arithmetic implementations
 * Arithmetic for FPGAs and reconfigurable logic
 * Design automation for computer arithmetic implementations
 * Arithmetic, datapath design and numerics for artificial intelligence, 
machine/deep learning
 * Computer arithmetic for approximate computing
 * Computer arithmetic for security and cryptography
 * Arithmetic to enhance accuracy or reliability (multiple-precision, interval 
arithmetic, ...)
 * Arithmetic challenges in HPC and exascale computing (accuracy, 
reproducibility, ...)
 * Arithmetic for specific application domains (big-data analytics, signal 
processing, computer graphics, multimedia, computer vision, finance, ...)
 * Computer arithmetic in emerging technologies
 * Non-conventional computer arithmetic and applications


=== Specific Sessions ===

Besides inviting submissions for regular sessions (8 pages maximum papers),
ARITH-2020 will also propose specific sessions. All accepted submissions, 
whether regular full papers, specific topics, short or industry papers or 
student forum presentations, will have a presentation slot scheduled.

-- Short and Industry Papers --

For ARITH-2020, we are also inviting short papers (4 pages maximum) to describe 
industry applications, work-in-progress ideas, or interim results. 
-- Specific Topic Sessions --

We are also inviting people to co-organize a few sessions on specific topics. 
Please identify the targeted session for submissions (e.g. use the anonymous 
author field). Submissions (4-page and 8-page) must comply to the procedure 
below and will be reviewed as all other types of sessions.

  Co-organizers have to contact the PC Chairsbefore Dec. 
30th, 2019 to propose a topic.

-- Student Forum --

We invite students at any level to present their work in an informal session 
without papers in the proceedings.


=== Procedure for submission for all sessions ===

An abstract submission deadline has been set to January 22nd (extended 
deadline). This initial submission must include title, author(s), keywords and 
abstract. The full paper is due on February 7th (extended deadline).

Submission site: https://easychair.org/conferences/?conf=arith2020

Papers under review elsewhere are not acceptable for submission to
ARITH-2020. A double-blind peer review policy will be enforced. Please,
remove authors' names, acknowledgments or any obvious references to the
authors before submission. By submitting a paper you implicitly confirm
you are solely submitting it to ARITH-2020. The final submissions of
accepted regular session papers cannot exceed 8 pages (NO extra pages)
using the IEEE Computer Society Conference format (two columns).
However, for review, authors may submit a paper with a maximum of 20
pages, 12pt font size, single column and double spacing. The final
submissions for short and industry papers cannot exceed 4 pages (NO
extra pages) using the IEEE Computer Society Conference format (two
columns). For review, the paper may have up to 10 pages, in 12pt font
size, single column and double spacing.

Formatting instructions:
http://www.ieee.org/conferences_events/conferences/publishing/templates.html

=== Important Dates 

Abstract submission (must include title,January 22nd, 2020
   authors, keywords, abstract)