GRLMC | 28 Feb 16:39 2015

AlCoB 2015: extended submission deadline 9 March

*To be removed from our mailing list, please respond to this message with
UNSUBSCRIBE in the subject line*

----------------------------------------------------------------------------
***** SUBMISSION DEADLINE EXTENDED: March 9 *****
----------------------------------------------------------------------------

****************************************************************************
******

2nd INTERNATIONAL CONFERENCE ON ALGORITHMS FOR COMPUTATIONAL BIOLOGY

AlCoB 2015

Mexico City, Mexico

August 4-6, 2015

Organized by:

Centre for Complexity Sciences (C3)
School of Sciences
Institute for Research in Applied Mathematics and Systems (IIMAS)
Graduate Program in Computing Science and Engineering
National Autonomous University of Mexico

Research Group on Mathematical Linguistics (GRLMC)
Rovira i Virgili University

http://grammars.grlmc.com/alcob2015/
(Continue reading)

Tijs van der Storm | 3 Mar 12:32 2015
Picon
Picon

DSLDI: 3rd Workshop on Domain-Specific Language Design and Implementation

*********************************************************************
FIRST CALL FOR TALK PROPOSALS

DSLDI 2015

Third Workshop on
Domain-Specific Language Design and Implementation

July 7, 2015
Prague, Czech Republic
Co-located with ECOOP

http://2015.ecoop.org/track/dsldi-2015-papers
*********************************************************************

Deadline for talk proposals: 2nd of April, 2015

If designed and implemented well, domain-specific languages (DSLs) combine the best features of
general-purpose programming languages (e.g., performance) with high productivity (e.g., ease of programming).

*** Workshop Goal ***

The goal of the DSLDI workshop is to bring together researchers and practitioners interested in sharing
ideas on how DSLs should be designed, implemented, supported by tools, and applied in realistic
application contexts. We are both interested in discovering how already known domains such as graph
processing or machine learning can be best supported by DSLs, but also in exploring new domains that could
be targeted by DSLs. More generally, we are interested in building a community that can drive forward the
development of modern DSLs.

*** Workshop Format ***
(Continue reading)

Andreas Abel | 27 Feb 19:56 2015
Picon
Picon

PhD position in dependent types/functional programming at Chalmers

We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:

   "The PhD student will join the Programming Logic group and contribute
   to its research on dependent type theory and functional programming.
   Topics of interest include the following directions of work:

   - Design of dependently typed functional programming languages.

   - Theory and implementation of type checkers, compilers etc. for
     dependently typed functional programming languages.

   - Investigations into the use of dependently typed functional
     programming languages, both as programming languages and as logical
     systems.

   - Models and applications of (homotopy) type theory."

Note that work on and in Agda matches several of the topics above.

Full text of the advertisement:

   http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=2902

Application deadline:

   March 31, 2015

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.
(Continue reading)

Andreas Abel | 27 Feb 19:55 2015
Picon
Picon

PhD position in dependent types/functional programming at Chalmers

We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:

   "The PhD student will join the Programming Logic group and contribute
   to its research on dependent type theory and functional programming.
   Topics of interest include the following directions of work:

   - Design of dependently typed functional programming languages.

   - Theory and implementation of type checkers, compilers etc. for
     dependently typed functional programming languages.

   - Investigations into the use of dependently typed functional
     programming languages, both as programming languages and as logical
     systems.

   - Models and applications of (homotopy) type theory."

Note that work on and in Agda matches several of the topics above.

Full text of the advertisement:

   http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=2902

Application deadline:

   March 31, 2015

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.
(Continue reading)

Andreas Abel | 27 Feb 19:55 2015
Picon
Picon

PhD position in dependent types/functional programming at Chalmers

We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:

   "The PhD student will join the Programming Logic group and contribute
   to its research on dependent type theory and functional programming.
   Topics of interest include the following directions of work:

   - Design of dependently typed functional programming languages.

   - Theory and implementation of type checkers, compilers etc. for
     dependently typed functional programming languages.

   - Investigations into the use of dependently typed functional
     programming languages, both as programming languages and as logical
     systems.

   - Models and applications of (homotopy) type theory."

Note that work on and in Agda matches several of the topics above.

Full text of the advertisement:

   http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=2902

Application deadline:

   March 31, 2015

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.
(Continue reading)

Nils Anders Danielsson | 27 Feb 19:41 2015
Picon
Picon

PhD student, dependent types/functional programming, Chalmers

We have an opening for a PhD student in dependent type theory and
functional programming at Chalmers. Here is an excerpt from the ad:

   "The PhD student will join the Programming Logic group and contribute
   to its research on dependent type theory and functional programming.
   Topics of interest include the following directions of work:

   - Design of dependently typed functional programming languages.

   - Theory and implementation of type checkers, compilers etc. for
     dependently typed functional programming languages.

   - Investigations into the use of dependently typed functional
     programming languages, both as programming languages and as logical
     systems.

   - Models and applications of (homotopy) type theory."

Note that work on and in Agda matches several of the topics above.

Full text of the advertisement:

   http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=2902

Application deadline:

   March 31, 2015
Thorsten Altenkirch | 27 Feb 17:25 2015
Picon
Picon

Midlands Graduate School 2015

Dear Colleagues,

The 2015 Midlands Graduate School will take place in Sheffield in April.
Please let your graduate students know, and anyone else who might be
interested in applying.

Thorsten Altenkirch

=====================================================


Call for Participation

MIDLANDS GRADUATE SCHOOL IN THE FOUNDATIONS OF COMPUTING SCIENCE

MGS 2015

07-11 April 2015, University of Sheffield


OVERVIEW

The Midlands Graduate School in the Foundations of Computing Science
(MGS) was established in 1999 as a collaboration between researchers
at the Universities of Birmingham, Leicester, Nottingham, and later
Sheffield. It has two main goals: to equip PhD students with a sound
basis for their research by deepening their knowledge on the
mathematical and conceptual foundations of computing; and to provide a
platform for making contacts with established researchers in the field
and with their peers who are at a similar stage in their research
careers.

This year's MGS is hosted by the Department of Computer Science at the
 University of Sheffield. It will start on April 07 and finish on April 11.

Information about previous events can be found at



PROGRAMME

MGS 2015 consists of nine courses, each with four or five hours of
lectures and exercise sessions. Three of the courses are introductory
or core; they should be taken by all participants. The other courses
are more advanced or specialised. Participants may select them
depending on their interests.

This year the invited lectures will be given by Prof Jeremy Gibbons,
Oxford.

In addition there will be early evening sessions in which participants
can briefly present and discuss their own research.

Core Courses:

* Category Theory, Roy Crole, Leicester
* Typed Lambda Calculus, Paul Blain Levy, Birmingham
* Patterns in Functional Programming, Jeremy Gibbons, Oxford

Advanced Courses: 

* Homotopy Type Theory, Thorsten Altenkirch, Nottingham 
* Infinite Data Structures, Venanzio Capretta, Nottingham
* Security Protocol Verification, Eike Ritter, Birmingham 
* Functional Reactive Programming, Neelakantan Krishnaswami, Birmingham 
* Building Verification Tools with Isabelle, Georg Struth, Sheffield


REGISTRATION

The registration deadline for MGS 2015 is Monday March 16. The
registration fee is £460 (a reduced fee without accommodation is
available on request).

Instructions for registation can be found at the MGS 2015 web site.


The registration fee includes 5 nights of accommodation with
 breakfasts at Hotel Ibis in Sheffield (from Monday April 06 evening
 to Saturday April 11 morning) as well as lunches, coffee breaks and
 the conference dinner.


TRAVEL

MGS 2015 takes place in the Sir Frederick Mappin Building of the
University of Sheffield. Information on traveling to Sheffield and
finding the venue can be found at the MGS 2015 web site. Train
station, hotel, lecture halls, restaurants and pubs are all within
walking distance.


ORGANISATION



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
Peter LeFanu Lumsdaine | 27 Feb 16:37 2015
Picon

CfP: UF/HoTT workshop, Warsaw, 29--30 June, with TLCA 2015

=============================================
CALL FOR PARTICIPATION
Workshop on Univalent Foundations and Homotopy Type Theory
(UF/HoTT, at TLCA 2015)
=============================================

-------------------------------------------------------------------------------

Workshop on Univalent Foundations and Homotopy Type Theory
29–30 June 2015, Warsaw, Poland
http://hott-uf.gforge.inria.fr
Co-located with RTA 2015 (RDP/TLCA)
Abstract submission deadline: 15 April

-------------------------------------------------------------------------------

Homotopy Type Theory/Univalent Foundations is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, informed by ideas and tools from abstract homotopy theory.

One practical goal of the programme is the computer formalisation of mathematics in such logical systems.  This workshop aims to focus on that aspect: bringing together researchers on formalisation in HoTT/UF to discuss the various established and experimental proof assistants for it, the different libraries available (HoTT Coq, UniMath, HoTT-Agda…), what logical features are convenient for the formalisation of “homotopical mathematics”, and how to make formalisation in HoTT/UF accessible and practical for mathematicians.
 
================
# Invited talks/tutorials:

* Benedikt Ahrens
* Thorsten Altenkirch
* Matthieu Sozeau
* Vladimir Voevodsky

================
# Submissions

* Abstract submission deadline: 15 April, 2015

Submissions should consist of a title and abstract, in pdf or text format, via https://easychair.org/conferences/?conf=hottuf15

Talks on practical formalisation are particularly solicited, but submissions on all UF/HoTT topics are welcome.

=================
# Program committee

* Benedikt Ahrens (Université Paul Sabatier, Toulouse)
* Steve Awodey (Carnegie Mellon University)
* Eric Finster (École Polytechnique)
* Dan Licata (Wesleyan University)
* Andrew Polonsky (VU University Amsterdam)
* Peter LeFanu Lumsdaine (Stockholm University)
* Nicolas Tabareau (Inria, Rennes)

=================
# Organisers

* Nicolas Tabareau (Inria, Rennes)
* Peter LeFanu Lumsdaine (Stockholm University)

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Jesper Cockx | 25 Feb 16:11 2015
Picon

How to install Epic for Agda?

Hi all,

Is there an easy way to install the Epic compiler for Agda? The page at http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Epic seems badly outdated. I've tried running 'cabal install epic' but this fails with the error:

Linking dist/build/epic/epic ...
make: Entering directory `/tmp/epic-0.9.3.2-13855/epic-0.9.3.2/evm'
gcc -Wall -O3 -DUSE_BOEHM   -c -o closure.o closure.c
In file included from closure.h:4:0,
                 from closure.c:1:
gc_header.h:10:19: fatal error: gc/gc.h: No such file or directory
 #include <gc/gc.h>
                   ^
compilation terminated.
make: *** [closure.o] Error 1
make: Leaving directory `/tmp/epic-0.9.3.2-13855/epic-0.9.3.2/evm'
Failed to install epic-0.9.3.2
cabal: Error: some packages failed to install:
epic-0.9.3.2 failed during the building phase. The exception was:
ExitFailure 2

According to the page at http://eb.host.cs.st-andrews.ac.uk/epic.php, this means I'm missing the Boehm garbage collector, for which there should be a debian package, but of which I cannot find the name.


Jesper
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Peter Divianszky | 25 Feb 12:03 2015
Picon

ANN: PandocAgda 2.4.3

PandocAgda [1] is a thin wrap around Agda which interprets comments in 
literate Agda files as markdown text [2].

The output of PandocAgda is similar to Agda HTML listings files [3], but 
with more formatting. An example can be seen in [4].

PandocAgda was rewritten such that it is now just 129 SLOC Haskell lines 
in one file [5].
This was possible after some refactoring on the Agda compiler sources.
This means that it will be quite easy to maintain PandocAgda in the future.

PandocAgda is usable right now, but if there is more interest, it can be 
improved in the following ways:

A)
PandocAgda could be moved into the agda/agda GitHub repository.
Basically this would add 3 files (PandocAgda.hs [5], PandocAgda.cabal 
[6], Agda.template [7]) to the repository and integrating it into the 
documentation.

B)
It seems feasible to produce LaTeX output with PandocAgda.
The benefit would be that one could use the LaTeX backend with the Agda 
compiler to format Agda source code with lightweight markdown syntax for 
formatting comments in Agda source code.

C)
Even it seems feasible to fully integrate Pandoc into PandocAgda.
The benefit would be to use Pandoc supported input in Agda source 
comments (including markdown, Textile, reStructuredText, HTML, LaTeX, 
MediaWiki markup, TWiki markup, Haddock markup, OPML, Emacs Org-mode, 
DocBook, txt2tags) and produce Pandoc supported output formats:
plain text, markdown, reStructuredText, XHTML, HTML 5, LaTeX (including 
beamer slide shows), ConTeXt, RTF, OPML, DocBook, OpenDocument, ODT, 
Word docx, GNU Texinfo, MediaWiki markup, DokuWiki markup, Haddock 
markup, EPUB (v2 or v3), FictionBook2, Textile, groff man pages, Emacs 
Org-Mode, AsciiDoc, InDesign ICML, and Slidy, Slideous, DZSlides, 
reveal.js or S5 HTML slide shows and PDF.

Are you interested in these improvements?

Cheers,

Peter

Links:

[1]: https://github.com/divipp/PandocAgda
[2]: http://johnmacfarlane.net/pandoc/README.html#pandocs-markdown
[3]: 
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.HowToGenerateWebPagesFromSourceCode
[4]: http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Recursive.html
[5]: https://github.com/divipp/PandocAgda/blob/master/PandocAgda.hs
[6]: https://github.com/divipp/PandocAgda/blob/master/PandocAgda.cabal
[7]: https://github.com/divipp/PandocAgda/blob/master/data/Agda.template
Kenichi Asai | 23 Feb 09:15 2015
Picon

Strictly positive

I am trying to encode in Agda the two-level types as introduced by
Sheard and Pasalic [1].  For example, I can encode the type for simple
types as follows:

----------------------------------
module main where

data t (Type : Set) : Set where
  TInt : t Type
  TArrow : Type -> Type -> t Type

data fix : Set where
  Fix : t fix -> fix
----------------------------------

where the parameter "Type" for t shows where the recursion occurs
(i.e., the two arguments of TArrow).  Now, I want to generalize t
to an arbitrary type (so that it can be given by users later).  I
considered:

----------------------------------
module Test (t : Set -> Set) where

data fix : Set where
  Fix : t fix -> fix
----------------------------------

but Agda complains:

> fix is not strictly positive, because it occurs in an argument to a
> bound variable in the type of the constructor Fix in the definition
> of fix.

Sure, if I instantiate t to:

t : Set -> Set
t Type = Type -> Type

it does lead to inconsistency.  But my intention is that I instantiate
t always as something that is strictly positive in its argument (like
the t for simple types above).  Is there any way to declare so, so
that fix can be defined independently of the definition of t?

Thank you in advance.

Sincerely,

[1] Tim Sheard and Emir Pasalic
"Two-level types and parameterized modules"
Journal of Functional Programming, 14(5):547-587, September 2004.

--

-- 
Kenichi Asai

Gmane