Faruk Caglar | 26 May 16:59 2015
Picon

Deadline Approaching - CFP: ACM SIGPLAN GPCE 2015

[Apologies if you receive multiple copies of this email]
-------------------------------------------------------------

 Call for Papers: Computer Languages, Systems and Structures
 COMLAN Special Issue on the 14th International Conference on
  Generative Programming: Concepts & Experiences (GPCE'15)

Papers will be selected among top ranked papers from GPCE'15:

                    ACM SIGPLAN GPCE 2015
              14th International Conference on
        Generative Programming: Concepts & Experiences

             Oct 26-27, 2015, Pittsburgh, PA, USA
                   http://www.gpce.org

GPCE keynote speaker: Prof. Priya Narasimhan (CMU, USA)

GPCE is co-located with:
ACM SIGPLAN conference on Systems, Programming, Languages and
Applications: Software for Humanity (SPLASH 2015)
and
ACM SIGPLAN 8th International Conference on Software Language
Engineering (SLE) 2015

-----------------------------------------------------------------
IMPORTANT DATES

  GPCE abstract submission  : June 8, 2015
  GPCE full paper submission: June 15, 2015
  GPCE authors notification : July 24, 2015
  GPCE camera-ready         : Aug 7, 2015
  GPCE conference           : Oct 26-27, 2015

  Special issue submission  : January 1, 2016
  Special issue notification: May 1, 2016
  Special issue publication : July 1, 2016

  Note that GPCE workshops are handled by SPLASH

All dates are Anywhere on Earth

-----------------------------------------------------------------
SCOPE

GPCE is a venue for researchers and practitioners interested in techniques
that use program generation, domain-specific languages, and component
deployment to increase programmer productivity, improve software quality,
and shorten the time-to-market of software products. In addition to
exploring cutting-edge techniques of generative software, our goal is to
foster further cross-fertilization between the software engineering and the
programming languages research communities.

-----------------------------------------------------------------
TOPICS OF INTEREST

GPCE seeks contributions on all topics related to generative software and
its properties. Topics of interest include, but are not limited to:

Generative software
* Domain-specific languages (language extension, language embedding,
  language design, language theory, language workbenches, interpreters,
  compilers)
* Product lines (domain engineering, feature-oriented and
  aspect-oriented programming, pre-processors, feature interactions)
* Metaprogramming (reflection, staging, partial evaluation), Type
  systems, Program synthesis
* Implementation techniques and tool support (components, plug-ins,
  libraries, metaprogramming, macros, templates, generic programming,
  run-time code generation, model-driven development, composition tools,
  code-completion and code-recommendation systems)

Practical Applications and Empirical evaluations
* Empirical evaluations of all topics above (user studies, substantial case
  studies, controlled experiments, surveys, rigorous measurements) 
* Application areas and engineering practice (Cloud Computing, Internet of
  Things, Cyber Physical Systems, Mobile Computing, Software Defined
  Networking, High Performance Computing, Patterns and Middleware,
  Development methods)

Properties of generative software
* Correctness of generators and generated code (analysis, testing, formal
  methods, domain-specific error messages, safety, security)  
* Reuse and evolution
* Modularity, separation of concerns, understandability, and
  maintainability 
* Performance engineering, nonfunctional properties (program optimization
  and parallelization, GPGPUs, multicore, footprint, metrics)

We particularly welcome papers that address some of the key challenges in
the field, such as,
* synthesizing code from declarative specifications
* supporting extensible languages and language embedding
* ensuring correctness and other nonfunctional properties of generated code
* proving generators correct
* improving error reporting with domain-specific error messages
* reasoning about generators
* handling variability-induced complexity in product lines
* providing efficient interpreters and execution languages
* human factors in developing and maintaining generators

GPCE encourages submissions about empirical evaluations and applications of
generative software, and such papers will be given special consideration
during reviewing.

-----------------------------------------------------------------
GPCE SUBMISSION GUIDELINES

Research papers: 10 pages maximum (ACM SIGPLAN style)

Research papers should report on original and unpublished results of
theoretical, empirical, conceptual, or experimental research that
contribute to scientific knowledge in the areas listed above (the PC chair
can advise on appropriateness)

Tool demos and short papers: 4 pages maximum (ACM SIGPLAN style).

The goal of short papers is to promote current work on research and
practice. Short papers represent an early communication of research and do
not always require complete results as in the case of a full paper. In this
way, authors can introduce new ideas to the community, discuss ideas and
get early feedback. Please note that short papers are not intended to be
position statements. Short papers are included in the proceedings and will
be presented with a shorter time slot at the conference.

Tool demonstrations should present tools that implement generative
techniques, and are available for use. Any of the GPCE topics of interest
are appropriate areas for tool demonstrations, although purely commercial
tool demonstrations will not be accepted. Submissions must provide a tool
description of 4 pages in SIGPLAN proceedings style (see above) and a
demonstration outline including screenshots of up to 4 pages. Tool
demonstrations must have the words "Tool Demo" or "Tool Demonstration" in
the title, possibly appended in parenthesis. The 4-page tool description
will, if the demonstration is accepted, be published in the proceedings.

-----------------------------------------------------------------
COMLAN SPECIAL ISSUE SUBMISSION GUIDELINES

The special issue will publish GPCE'15 papers by invitation from the
guest editors, is closed to papers outside the conference, and will
only include top-ranked papers from GPCE'15 (based on the GPCE'15
review, see scope and topics of interest, above).  The special issue
will be published by Elsevier in Computer Languages, Systems and
Structures (COMLAN):

http://www.journals.elsevier.com/computer-languages-systems-and-structures/

-----------------------------------------------------------------
ORGANIZERS

GENERAL CHAIR

  Christian Kastner, Carnegie Mellon University, Pittsburgh, PA, USA

PROGRAM COMMITTEE CHAIR

  Aniruddha Gokhale, Vanderbilt University, Nashville, TN, USA

PUBLICITY CO-CHAIRS

  Faruk Caglar, Vanderbilt University, Nashville, TN, USA
  Tomofumi Yuki, INRIA Rhone-Alpes, France
 
SPECIAL ISSUE GUEST EDITORS

  Ulrik Pagh Schultz, University of Southern Denmark, Denmark
  Kenichi Asai, Ochanomizu University, Japan
  Aniruddha Gokhale, Vanderbilt University, Nashville, TN, USA

PROGRAM COMMITTEE

  Kenichi Asai, Ochanomizu Univ, Japan
  Emilie Balland, INRIA Bordeaux, France
  Don Batory, Univ of Texas, USA
  Walter Binder, Univ of Lugano, Switzerland
  Jan Bosch, Chalmers Univ, Sweden
  Akshay Dabholkar, Oracle, USA
  Ewen Denney, NASA Ames, USA
  Katrina Falkner, Univ of Adelaide, Australia
  Bernd Fischer, Stellenbosch Univ, South Africa
  Matthew Flatt, Univ of Utah, USA
  Jeff Gray, Univ of Alabama, USA
  Michael Haupt, Oracle Labs, Germany
  James Hill, Indiana Univ Purdue Univ at Indianapolis, USA
  Young-Woo Kwon, Utah State Univ, USA
  Raffaela Mirandola, Politechnico di Milano, Italy
  Hridesh Rajan, Iowa State Univ, USA
  Laurent Reveillere, LaBRI, Univ of Bordeaux, France
  Marcio Ribeiro, Federal Univ of Alagoas, Brazil
  Tiark Rompf, Purdue Univ, USA
  Klaus Schmid, Stiftung Universitat Hildesheim, Germany
  Norbert Siegmund, Univ of Passau, Germany
  Yannis Smaragdakis, Univ of Athens, Greece
  Sumant Tambe, RTI Inc, USA
  Petr Tuma, Charles Univ, Czech Republic
  Nalini Venkatasubramanian, Univ of California, Irvine, USA
  Jules White, Vanderbilt Univ, USA
  Eric Wohlstadter, Univ of British Columbia, Canada
 







_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andrés Sicard-Ramírez | 26 May 02:14 2015
Picon

ANNOUNCE: Agda 2.4.2.3 release

Hi,

We would like to announce the release of Agda 2.4.2.3.

Install with

  $ cabal update && cabal install Agda

or got to

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

Important changes since Agda 2.4.2.2:

  http://hackage.haskell.org/package/Agda-2.4.2.3/changelog

For the time being, a version of the standard library compatible with
Agda 2.4.2.3 is available via (requires Git >= 1.7.10)

  $ git clone https://github.com/agda/agda-stdlib.git --branch 2.4.2.3
--single-branch

or using previous versions of Git

  $ git clone https://github.com/agda/agda-stdlib.git
  $ cd agda-stdlib/
  $ git checkout 2.4.2.3

All the best,

--

-- 
Andrés, on behalf of the Agda team
Andrés Sicard-Ramírez | 19 May 05:56 2015
Picon

ANNOUNCE: Agda 2.4.2.3 release candidate

Hi,

We would like to announce a release candidate for Agda 2.4.2.3:

  https://github.com/agda/agda/archive/2.4.2.2.20150518.tar.gz

This RC can be installed using the following instructions:

  $ tar xzf 2.4.2.2.20150518.tar.gz
  $ cd Agda-2.4.2.2.20150518.tar.gz
  $ cabal install

Important changes since Agda 2.4.2.2:

  https://github.com/agda/agda/blob/2.4.2.2.20150518/CHANGELOG

Please test as much as possible.

Best,

--

-- 
Andrés, on behalf of the Agda team
Martin Escardo | 15 May 21:47 2015
Picon
Picon

literate colours

In a literate Agda file when rendered with agda --html, the comments are
red.

But in the way I use literate Agda, the comments are the substance and
the code is the form of the substance.

The substance shouldn't be red - plain black would work better with me.

How can I change the colours of the substance and the form?

Thanks,
Martin
Sebastian Erdweg | 14 May 08:36 2015
Picon

Deadline extension: Workshop on Generic Programming 2015 - New deadline May 22

Submission deadline extended to May 22

======================================================================
                      CALL FOR PAPERS

                          WGP 2015

       11th ACM SIGPLAN Workshop on Generic Programming
                     Vancouver, Canada
                   Sunday, August 30, 2015

               http://www.wgp-sigplan.org/2015

                     Co-located with the
International Conference on Functional Programming (ICFP 2015)
======================================================================

Goals of the workshop
---------------------

Generic programming is about making programs more adaptable by making
them more general. Generic programs often embody non-traditional kinds
of polymorphism; ordinary programs are obtained from them by suitably
instantiating their parameters. In contrast with normal programs, the
parameters of a generic program are often quite rich in structure; for
example they may be other programs, types or type constructors, class
hierarchies, or even programming paradigms.

Generic programming techniques have always been of interest, both to
practitioners and to theoreticians, and, for at least 20 years,
generic programming techniques have been a specific focus of research
in the functional and object-oriented programming communities. Generic
programming has gradually spread to more and more mainstream
languages, and today is widely used in industry. This workshop brings
together leading researchers and practitioners in generic programming
from around the world, and features papers capturing the state of the
art in this important area.

We welcome contributions on all aspects, theoretical as well as
practical, of

* generic programming,
* programming with (C++) concepts,
* meta-programming,
* programming with type classes,
* programming with modules,
* programming with dependent types,
* type systems for generic programming,
* polytypic programming,
* adaptive object-oriented programming,
* component-based programming,
* strategic programming,
* aspect-oriented programming,
* family polymorphism,
* object-oriented generic programming,
* implementation of generic programming languages,
* static and dynamic analyses of generic programs,
* and so on.

Program Committee
-----------------

* Patrick Bahr (co-chair), University of Copenhagen
* Sebastian Erdweg (co-chair), Technical University of Darmstadt
* Edwin Brady, University of St Andrews
* Edsko de Vries, Well-Typed LLP
* Mauro Jaskelioff, National University of Rosario
* Johan Jeuring, Utrecht University
* Pieter Koopman, Radboud University Nijmegen
* Bruno C. d. S. Oliveira, University of Hong Kong
* Nicolas Pouillard, IT University of Copenhagen
* Sukyoung Ryu, Korea Advanced Institute of Science and Technology
* Sibylle Schupp, Hamburg University of Technology
* Sam Tobin-Hochstadt, Indiana University

Proceedings and Copyright
-------------------------

We plan to have formal proceedings, published by the ACM. Accepted
papers will be included in the ACM Digital Library. Authors must grant
ACM publication rights upon acceptance
(http://authors.acm.org/main.html), but may retain copyright if they
wish. Authors are encouraged to publish auxiliary material with their
paper (source code, test data, and so forth). The proceedings will be
freely available for download from the ACM Digital Library from one
week before the start of the conference until two weeks after the
conference.

Submission details
------------------

* Submission deadline:  Fri, 22nd May 2015
* Author notification:  Fri, 26th June 2015
* Final version due:    Sun, 19th July 2015
* Workshop:             Sun, 30th August 2015

Submitted papers should fall into one of two categories:

* Regular research papers (12 pages)
* Short papers: case studies, tool demos, generic pearls (6 pages)

Regular research papers are expected to present novel and interesting
research results. Short papers need not present novel or fully polished
results. Good candidates for short papers are those that report on 
interesting case studies of generic programming in open source or 
industry, present demos of generic programming tools or libraries, 
or discuss elegant and illustrative uses of generic programming ('pearls').

All submissions should be in portable document format (PDF), formatted
using the ACM SIGPLAN style guidelines (two-column, 9pt). Regular 
research papers must not exceed 12 pages. Short papers must not exceed 
6 pages. If applicable, papers should be marked with one of the labels
'case study, 'tool demo' or 'generic pearl' in the title at the time 
of submission.

Papers should be submitted via HotCRP at

https://icfp-wgp15.hotcrp.com/

Travel Support
--------------

Student attendees with accepted papers can apply for a SIGPLAN PAC grant
to help cover travel expenses. PAC also offers other support, such as
for child-care expenses during the meeting or for travel costs for
companions of SIGPLAN members with physical disabilities, as well as for
travel from locations outside of North America and Europe. For details
on the PAC program, see its web page (http://www.sigplan.org/PAC.htm).

History of the Workshop on Generic Programming
----------------------------------------------

Earlier Workshops on Generic Programming have been held in

* Gothenburg, Sweden 2014 (affiliated with ICFP),
* Boston, Massachusetts, US 2013 (affiliated with ICFP),
* Copenhagen, Denmark 2012 (affiliated with ICFP),
* Tokyo, Japan 2011 (affiliated with ICFP),
* Baltimore, Maryland, US 2010 (affiliated with ICFP),
* Edinburgh, UK 2009 (affiliated with ICFP),
* Victoria, BC, Canada 2008 (affiliated with ICFP),
* Portland 2006 (affiliated with ICFP),
* Ponte de Lima 2000 (affiliated with MPC),
* Marstrand 1998 (affiliated with MPC).

Furthermore, there were a few informal workshops

* Utrecht 2005 (informal workshop),
* Dagstuhl 2002 (IFIP WG2.1 Working Conference),
* Nottingham 2001 (informal workshop).

There were also (closely related) DGP workshops in Oxford (June
3-4 2004), and a Spring School on DGP in Nottingham (April 24-27
2006, which had a half-day workshop attached).

WGP Steering Committee
----------------------

* Andres Löh
* Ronald Garcia
* Jacques Carette
* Jeremiah Willcock
* José Pedro Magalhães
* Tiark Rompf
* Tarmo Uustalo
* Stephanie Weirich
* Fritz Henglein

_______________________________________________
ecoop-info mailing list
ecoop-info@...
http://web.satd.uma.es/mailman/listinfo/ecoop-info
Andrew Pitts | 13 May 15:00 2015
Picon
Picon

Quotient types in Agda, if you Trust Me

Wouldn't it be nice to have quotient types in Agda?

By quotient types I mean that given any type A : Set and any relation
R : A -> A -> Set, there should be a type A / R : Set and a function
_mod R : A -> A / R for which there is a proof
equ : {x y : A}(r : R x y) -> x mod R ≡ y mod R and which is
category-theoretically universal, in a suitable sense, with this
property.

One can use such types to avoid "setoid hell". And they make function
extensionality derivable.

I am happy to have this just for h-sets, that is, to have something
that works when we allow Agda to use full dependent pattern matching
and hence can prove uniqueness of identity proofs.

The attached file (quotient.agda) is a way of providing such quotient
types using an enhanced version of Dan Licata's trick with "private"
and "postulate" declarations to define an interval type

<http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/>

The enhancements are two-fold:

1. Use primTrustMe rather than postulates for improved computational
behaviour, inspired by Alan Jeffrey's recent post to this list:

<https://groups.google.com/forum/#!topic/homotopytypetheory/hTAVT6CGbrs>

2. Careful combination of thunking and private declarations to ensure
(we hope!) that the function _mod R : A -> A / R sending an element to
its equivalence class cannot be proved to be an injection outside the
scope of the private declarations. (It is injective with the private
declations, and if it could be proved injective outside their scope,
one can easily derive a logical contradiction.) This is adapted from
the hott-agda development

<https://github.com/dlicata335/hott-agda/blob/master/lib/spaces/hithacks.agda>

of Dan Licata, Guillaume Brunerie, Eric Finster and Dan Grayson. The
"thunking Yoga" used to avoid logical inconsistency in quotient.agda at
first seems more complicated than it need be. But we (Dan Licata, Alan
Jeffrey and I) were able to break simpler schemes.

So here's a challenge.

Can anyone fill the hole in

open import quotient

data Empty : Set where

contradiction : Empty
contradiction = {!!}

without any further use of primTrustMe or postulate?

Or convince me that that is not possibe?

Andy Pitts
Attachment (quotient.agda): application/octet-stream, 14 KiB
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Kenichi Asai | 13 May 09:38 2015
Picon

documents on the implementation of agda2-mode?

Are there any documents describing how agda2-mode is implemented?  I
found the interactive goals (in the form { }0) used in agda2-mode are
very useful and want to have such mechanism for other purposes, too.
Do I have to read the emacs lisp files?  Thanks in advance.

Sincerely,

--

-- 
Kenichi Asai
publicityifl | 10 May 22:02 2015
Picon

First Call for Papers for IFL 2015

Hello,

Please, find below the first call for papers for IFL 2015.
Please forward these to anyone you think may be interested.
Apologies for any duplicates you may receive.

best regards,
Jurriaan Hage
Publicity Chair of IFL

---

IFL 2015 - Call for papers

27th SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES - IFL 2015

University of Koblenz-Landau, Koblenz, Germany

In cooperation with ACM SIGPLAN

September 14-16, 2015

http://ifl2015.wikidot.com/

Scope

The goal of the IFL symposia is to bring together researchers actively engaged in the implementation and
application of functional and function-based programming languages. IFL 2015 will be a venue for
researchers to present and discuss new ideas and concepts, work in progress, and publication-ripe
results related to the implementation and application of functional languages and function-based programming.

Peer-review

Following the IFL tradition, IFL 2015 will use a post-symposium review process to produce the formal
proceedings. All participants of IFL2015 are invited to submit either a draft paper or an extended
abstract describing work to be presented at the symposium. At no time may work submitted to IFL be
simultaneously submitted to other venues; submissions must adhere to ACM SIGPLAN's republication policy:

http://www.sigplan.org/Resources/Policies/Republication

The submissions will be screened by the program committee chair to make sure they are within the scope of
IFL, and will appear in the draft proceedings distributed at the symposium. Submissions appearing in the
draft proceedings are not peer-reviewed publications. Hence, publications that appear only in the
draft proceedings do not count as publication for the ACM SIGPLAN republication policy. After the
symposium, authors will be given the opportunity to incorporate the feedback from discussions at the
symposium and will be invited to submit a revised full article for the formal review process. From the
revised submissions, the program committee will select papers for the formal proceedings considering
their correctness, novelty, originality, relevance, significance, and clarity.

Important dates

August 10: Submission deadline draft papers
August 12: Notification of acceptance for presentation
August 14: Early registration deadline
August 21: Late registration deadline
September 7: Submission deadline for pre-symposium proceedings
September 14-16: IFL Symposium
December 1: Submission deadline for post-symposium proceedings
January 15, 2016: Notification of acceptance for post-symposium proceedings
March 1, 2016: Camera-ready version for post-symposium proceedings

Submission details

Prospective authors are encouraged to submit papers or extended abstracts to be published in the draft
proceedings and to present them at the symposium. All contributions must be written in English. Papers
must adhere to the standard ACM two columns conference format. For the pre-symposium proceedings we
adopt a 'weak' page limit of 12 pages. For the post-symposium proceedings the page limit of 12 pages is
firm. A suitable document template for LaTeX can be found at:

http://www.acm.org/sigs/sigplan/authorInformation.htm

Authors submit through EasyChair:

https://easychair.org/conferences/?conf=ifl2015

Topics

IFL welcomes submissions describing practical and theoretical work as well as submissions describing
applications and tools in the context of functional programming. If you are not sure whether your work is
appropriate for IFL 2015, please contact the PC chair at rlaemmel@...
Topics of interest include, but are not limited to:

- language concepts
- type systems, type checking, type inferencing
- compilation techniques
- staged compilation
- run-time function specialization
- run-time code generation
- partial evaluation
- (abstract) interpretation
- metaprogramming
- generic programming
- automatic program generation
- array processing
- concurrent/parallel programming
- concurrent/parallel program execution
- embedded systems
- web applications
- (embedded) domain specific languages
- security
- novel memory management techniques
- run-time profiling performance measurements
- debugging and tracing
- virtual/abstract machine architectures
- validation, verification of functional programs
- tools and programming techniques
- (industrial) applications

Peter Landin Prize

The Peter Landin Prize is awarded to the best paper presented at the symposium every year. The honored
article is selected by the program committee based on the submissions received for the formal review
process. The prize carries a cash award equivalent to 150 Euros.

Programme committee

Chair: Ralf Lämmel, University of Koblenz-Landau, Germany

- Malgorzata Biernacka, University of Wroclaw, Poland
- Laura M. Castro, University of A Coruña, Spain
- Martin Erwig, Oregon State University, USA
- Dan Ghica, University of Birmingham, UK
- Andrew Gill, University of Kansas, USA
- Stephan Herhut, Google, USA
- Zhenjiang Hu, National Institute of Informatics (NII), Japan
- Mauro Jaskelioff, CIFASIS/Universidad Nacional de Rosario, Argentina
- Frédéric Jouault, ESEO, France
- Oleg Kiselyov, Tohoku University, Japan
- Lindsey Kuper, Indiana University, USA
- Rita Loogen, Philipps-Universität Marburg, Germany
- Akimasa Morihata, University of Tokyo, Japan
- Atsushi Ohori, Tohoku University, Japan
- Bruno C. D. S. Oliveira, The University of Hong Kong, Hong Kong
- Frank Piessens, Katholieke Universiteit Leuven, Belgium
- Norman Ramsey, Tufts University, USA
- Matthew Roberts, Macquarie University, Australia
- Manfred Schmidt-Schauss, Goethe-University Frankfurt, Germany
- Simon Thompson, University of Kent, UK
- Stephanie Weirich, University of Pennsylvania, USA
- Steve Zdancewic, University of Pennsylvania , USA

Venue

The 27th IFL will be held in association with the Faculty of Computer Science, University of
Koblenz-Landau, Campus Koblenz. Koblenz is well connected by train to several international airports.
For instance, Koblenz can be reached from Frankfurt by high-speed train ICE within an hour. The modern
Koblenz campus is close to the city center and can be reached by foot, bus, or cab. See the website for more
information on the venue.
Thorsten Altenkirch | 8 May 15:18 2015
Picon
Picon

PhD studentship in Nottingham available

Hi,

There is one fully funded PhD studentship available (for EU citizens) in Nottingham with me as a supervisor. The studentship is related to a grant on Homotopy Type Theory supported by the UK EPSRC jointly with Nicola Gambino in Leeds and Neil Ghani and Conor McBride at the University of Strathclyde in Glasgow. 

Homotopy Type Theory (HoTT) is a revolutionary new approach to type theory where types are interpreted as spaces, terms as points and equalities as paths. Decades of research in homotopy theory has uncovered the structure of such paths and HoTT uses this structure as the basis of a new theory of equality. Excitingly, within homotopy theory, one naturally studies higher homotopies of paths between paths and this gives the higher dimensional structure of equality we previously lacked. The objective of this grant is to translate the advances of HoTT into more concrete programming language and verification tools.

The prospective student should have a background in Computer Science and/or Mathematics and have a keen interest in logic, foundations of Computer Science and Mathematics and Programming Languages. A good knowledge of functional programming is helpful. Successful applicants should have completed (or will complete soon) an MSc with a (predicted) first class classification or comparable. Good communication skills and the ability to work with the thriving group in Nottingham and to interact with our colleagues in Strathclyde and Leeds are important assets.

The studentship will cover PhD tuition fees and a tax free stipend for three years (£13,590 for the 2014-15 academic year) for UK/EU students. For international students it is possible to apply for additional funding via the University of Nottingham to bridge the difference but this is subject to tight deadlines and an additional selection process. Funding is for 3 years, completion of PhD has to happen within 4 years.

Applicants should email Thorsten.Altenkirch-QabDm/c3fAmwa9SdKMSz+Q@public.gmane.org with:

an up-to-date CV, including the email addresses of 1 - 2 relevant  academic references; 
transcript and/or certificates (scanned);
a short (1 - 2 pages) research proposal;
1-2 examples of their work (eg slides of talks, projects, thesis) in electronic form; and
a cover letter (or email) explaining their reasons to apply for this position (< 500 words).

If you have applied for an earlier advert in December but not been successful, let me know wether you are still interested in the position.If you have questions, please don’t hesitate to contact me by email.  Note that unlike the earlier advert this time the studentship is limited to people from the EU due to funding restrictions.

Thorsten

P.S. Please feel free to forward this email to potentially interested people.



This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Maciej Pirog | 5 May 22:40 2015
Picon
Picon

Summer School on Generic and Effectful Programming

Call for Participation

          SUMMER SCHOOL ON GENERIC AND EFFECTFUL PROGRAMMING

           St Anne's College, Oxford, 6th to 10th July 2015
             http://www.cs.ox.ac.uk/projects/utgp/school/
			    
TOPIC

Generic programming is a technique that exploits the inherent
structure that exists in data, to automatically produce efficient and
flexible algorithms that can be adapted to suit different needs. The
goal of this school is to explore datatype-generic programming and
related topics from a variety of different angles, emphasizing in
particular the interplay of generics and effects.

This summer school is the closing activity of the EPSRC-funded project
"Unifying Theories of Generic Programming" at Oxford University.

LECTURERS

Six lecturers from the Programming Languages community, each an
acknowledged expert in their specialism, will cover various aspects of
generic and effectful programming. Each will give about four hours'
lectures, distributed throughout the week.

  Edwin Brady (University of St Andrews)
  "Embedded Domain-Specific Languages in Idris"

  Fritz Henglein (University of Copenhagen)
  "Worst-case Efficient Generic Functional Programming on Bulk Data"

  Andres Löh (Well-Typed)
  "Applying Type-level and Generic Programming in Haskell"

  Conor McBride (University of Strathclyde)
  "Datatypes of Datatypes"

  Don Syme (Microsoft Research)
  "Compile-time Meta-programming for the Information-rich World"

  Tarmo Uustalu (Tallinn University of Technology)
  "Containers for Effects and Contexts"

PREREQUISITES

The school is aimed at doctoral students in programming languages and
related areas; however, researchers and practitioners will be very
welcome, as will strong masters students with the support of a
supervisor. It will be assumed that participants have a good
understanding of typed functional programming, as in Haskell, O'Caml,
or F#.

DATES

Registration deadline: 21st June 2015
School:                6th July (9am) to 10th July 2015 (lunchtime)

COSTS

Costs will be kept low, thanks to support from EPSRC. There will be a
nominal registration fee of £135, and B&B accommodation in college
will be £75 (ensuite) or £48 (shared bathroom) per night. We can
accept at most 50 participants; places will be allocated on a
first-come, first-served basis.

FURTHER INFORMATION

Further information, including instructions on how to register, is
available at the website:

  http://www.cs.ox.ac.uk/projects/utgp/school/
Ralph Matthes | 5 May 13:19 2015
Picon
Picon

FICS'15 Call for papers - Fixed Points in Computer Science (CSL'15 workshop 11+12 sept. 2015)

Call for Papers

*** FICS 2015 ***

  http://www.irit.fr/FICS2015/

               International Workshop on Fixed Points in Computer Science
               Berlin, 11-12 September 2015
               satellite of the International Conference CSL 2015
               (Computer Science Logic)

IMPORTANT DATES

Abstract submission:         Monday, June 16
Paper submission:            Monday, June 23
Notification:                Monday, July 27
Final version:               Monday, August 24

BACKGROUND

Fixed points play a fundamental role in several areas of computer science.
They are used to justify (co)recursive definitions and associated reasoning
techniques. The construction and properties of fixed points have been
investigated in many different settings such as: design and implementation
of programming languages, logics, verification, databases.

The aim of this workshop is to provide a forum for researchers to present
their results to those members of the computer science and logic communities
who study or apply the theory of fixed points.

Topics include, but are not restricted to:

   * fixed points in algebra and coalgebra
   * fixed points in formal languages and automata
   * fixed points in game theory
   * fixed points in programming language semantics
   * fixed points in the mu-calculus and modal logics
   * fixed points in process algebras and process calculi
   * fixed points in functional programming and type theory
   * fixed points in relation to dataflow and circuits
   * fixed points in logic programming and theorem proving
   * fixed points in finite model theory, descriptive complexity theory,
     and databases
   * fixed points in category theory for logic in computer science

PROGRAM COMMITTEE

  Ulrich Berger (Swansea Univ.)
  Dietmar Berwanger (CNRS & ENS Cachan)
  Filippo Bonchi (CNRS & ENS Lyon)
  Venanzio Capretta (Univ. Nottingham)
  Krishnendu Chatterjee (Institute of Science and Technology Austria)
  Kaustuv Chaudhuri (INRIA Saclay & École Polytechnique)
  Thomas Colcombet (CNRS & Univ. Paris Diderot)
  Makoto Hamana (Gunma Univ.)
  Radu Mardare (Aalborg Univ.)
  Ralph Matthes (co-chair, CNRS & Univ. Toulouse)
  Henryk Michalewski (Univ. Warsaw)
  Matteo Mio (co-chair, CNRS & ENS Lyon)
  Andrzej Murawski (Univ. Warwick)
  Alexandra Silva (Radboud Univ. Nijmegen)
  Sam Staton (Univ. Oxford)

TWO INVITED SPEAKERS

   * To be announced

SUBMISSION

The selection of contributed talks will be based on extended abstracts/short
papers describing original results in sufficient detail to constitute a
publication. Submission is via EasyChair:
   https://easychair.org/conferences/?conf=fics2015

Accepted papers will be published through the open-access venue EPTCS.
Submissions should be composed using LaTeX and, preferably, using the
EPTCS style:
   http://style.eptcs.org/

Typical submissions would be 8 pages long but submissions in the range
[6,15] pages will be considered acceptable. If you have good reasons to
go below the lower bound, then please contact the PC chairs before
submission.

JOURNAL PUBLICATION

If the number and quality of submissions justifies it, a subsequent
special issue of a journal will be prepared with extended versions of
selected papers. A special issue of FICS 2013 is in preparation and
will appear in Fundamenta Informaticae.

Gmane