Arnaud Durand | 17 May 2013 18:38
Picon

LCC'13 : Workshop on Logic and Computational Complexity

[ Please broadcast/post/forward.   Apologies for duplicates]

LCC'13 WORKSHOP ANNOUNCEMENT

The Fourteenth International Workshop on Logic and Computational Complexity
(LCC'11,http://www.cs.swansea.ac.uk/lcc2013/)
will be held in Torino on September 6, 2013, as an affiliated meeting
of CSL'13 (http://csl13.di.unito.it/).

LCC meetings are aimed at the foundational interconnections between 
logic and computational complexity, as present, for example,  in 
implicit computational complexity (descriptive and type-theoretic 
methods); deductive formalisms as they relate to complexity (e.g. 
ramification, weak comprehension, bounded arithmetic, linear logic and 
resource logics); complexity aspects of finite model theory and 
databases; complexity-mindful program derivation and verification; 
computational complexity at higher type; and proof complexity.

The LCC'13 program will consist of invited lectures as well as selected 
contributed papers. We welcome informal presentations about work in 
progress, survey papers, as well as work submitted or published 
elsewhere, provided all pertinent information is disclosed at submission 
time.  Submissions in the form of an extended abstract of approx. 5 
pages are welcome. If full papers are submitted, they should not exceed 
15 pages.  Proposed papers should be sent to the program chairs.

IMPORTANT DATES

Paper submission deadline:       20 June
Authors' notification:            8 July
(Continue reading)

Sergei Meshveliani | 17 May 2013 10:57
Picon

isHead x (x :: xs)

Please, how to prove the following?

  isHead : ℕ → List ℕ → Bool
  isHead _ []        = false 
  isHead x (y ∷ ys)  with  x ≟ y
  ...              | yes _ = true 
  ...              | no _  = false 

  isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
  isHP x xs =
              ??

Thanks,

------
Sergei
S B Cooper | 16 May 2013 14:06
Picon
Favicon

CiE 2013 in Milan, July 1 - 5: First Call for Participation

---------------------------------------------------------------------------
       COMPUTABILITY IN EUROPE 2013: The Nature of Computation
                       Milan, Italy,  July  1 - 5, 2013

                           CALL FOR PARTICIPATION

                 Informal Presentation Deadline: 31 May 2013
                   Early Registration Deadline: 31 May 2013

                      http://cie2013.disco.unimib.it

                 co-located with
         Unconventional Computation and Natural Computation 2013

             http://ucnc2013.disco.unimib.it
---------------------------------------------------------------------------

TUTORIAL SPEAKERS:  Gilles Brassard (Universite de Montreal) and
Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and 
University of Colorado at Boulder)

PLENARY TALKS:
Ulle Endriss (University of Amsterdam)
Lance Fortnow (Georgia Institute of Technology)
Anna Karlin (University of Washington)
Bernard Moret (Ecole Polytechnique Federale de Lausanne)
Mariya Soskova (Sofia University)
Endre Szemeredi (Hungarian Academy of Sciences, Rutgers University)

SPECIAL SESSIONS:
(Continue reading)

edprocess | 17 May 2013 07:20

Final CFP: INTECH 2013 at BCS

Call for Papers 

The Third International Conference on Innovative Computing Technology 
(INTECH 2013)
August 29-31, 2013
British Computer Society, London, UK
Technically co-sponsored by IEEE UK & RI
Proceedings will be indexed in IEEE Xplore
(Http://www.dirf.org/intech) 

The First international conference on Innovative Computing Technology 
(INTECH 2011) was held at Sao Carlos in Brazil followed by the Second 
International Conference on Innovative Computing Technology (INTECH 2012) at 
Casablanca in Morocco. The third conference will be held at British Computer 
Society during August 29-31, 2013. The INTECH 2013 offers the opportunity 
for institutes, research centers, engineers, scientists and industrial 
companies to share their latest investigations, researches, developments and 
ideas in area of Innovative Computing Technology, which covers huge topics. 
The INTECH intends to address various innovative computing techniques 
involving various applications. This forum will address a large number of 
themes and issues. The conference will feature original research and 
industrial papers on the theory, design and implementation of computing 
technologies, as well as demonstrations, tutorials, workshops and industrial 
presentations. 

This conference (INTECH 2013) will include presentations of contributed 
papers by invited keynote speakers. 

Conference papers will include innovative computing paradigms in the 
following topics: 
(Continue reading)

Stephanie Weirich | 16 May 2013 19:38
Favicon
Gravatar

DTP 2013 2nd Call For Papers

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

                               DTP 2013

           ACM SIGPLAN Workshop on Dependently-Typed Programming

                             24th SEPTEMBER 2013
                          Boston, Massachusetts, USA                    
                       (co-located with ICFP 2013)

                          2nd CALL FOR PAPERS

             http://www.seas.upenn.edu/~sweirich/dtp13
========================================================================

[NOTE: Compared to the first announcement, this CFP updates the workshop 
date, submission deadline, and also solicits informal presentations for DTP.]

Overview
--------

The ACM SIGPLAN Workshop on Dependently-Typed Programming 2013 will be
co-located with the [2013 International Conference on Functional Programming
(ICFP), in Boston, Massachusetts, USA](http://icfpconference.org/icfp2013/).

The purpose of DTP is to discuss experiences with dependent types in
programming and future developments for dependently-typed languages. Recent
years have seen increasing overlap between the dependent type theory and
functional programming languages communities. Co-locating this workshop with
ICFP will promote that cross fertilization.
(Continue reading)

Guillaume Brunerie | 15 May 2013 21:05
Picon

Defining a module by pattern matching

Hi,

I have several definitions all starting with the following arguments:
{x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}

In order to make the code more readable, I would like to wrap them in
a section so that I can write the arguments only once.
The issue is that all those definitions are defined by pattern
matching on p, so I cannot do it and I need to copy paste the list of
arguments for each definition which makes the code quite hard to read.

Is there a way to workaround this issue? Some way to define a
parametrized module by pattern matching, or something like that?

Thanks,

Guillaume
Luca Paolini | 14 May 2013 09:53
Picon
Favicon

RDP 2013 Call for Participation

*********************************************************************
*** Federated Conference on Rewriting, Deduction, and Programming ***
***                            RDP 2013                           ***
***                    June 23 - June 28, 2013                    ***
***                   Eindhoven, The Netherlands                  ***
***                 http://www.win.tue.nl/rdp2013/                ***
***                                                               ***
***                     CALL FOR PARTICIPATION                    ***
***                                                               ***
*********************************************************************

*************   EARLY REGISTRATION CLOSES ON JUNE 1     *************

---------------------------------------------------------------------
-- REGISTRATION --
---------------------------------------------------------------------

For online registration visit:
   http://www.win.tue.nl/rdp2013/reg.html

Early registration closes on June 1.

---------------------------------------------------------------------
-- ABOUT RDP --
---------------------------------------------------------------------

RDP'13 is the seventh edition of the biannual Federated Conference on
Rewriting, Deduction, and Programming, consisting of two main
conferences and related events.

(Continue reading)

Sergei Meshveliani | 14 May 2013 10:32
Picon

`abstract' on Web keywords

People,
I try to find the manual on `abstract' in the Web reference manual on

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Keywords

Clicking at `data' shows the docs on `data'.

But clicking at `abstract'  displays several sections on modules where I
do not find the word `abstract'.
Am I missing something?

Thanks,

------
Sergei
Tillmann Rendel | 13 May 2013 14:34
Picon
Favicon
Gravatar

Instance arguments and hole types

Hi,

I'm trying to use Agda's instance arguments to overload the ⟦_⟧ function 
for various different types of syntax, and it works. But it is less 
convenient than I hoped, because sometimes, the Emacs mode shows the 
overloading plumbing instead of inlining it away.

Here's what I have, starting with the overloading apparatus:
> open import Level
>
> record Meaning (Syntax : Set) {ℓ : Level} : Set (suc ℓ) where
>   constructor
>     meaning
>   field
>     Semantics : Set ℓ
>     ⟦_⟧ : Syntax → Semantics
>
> open Meaning {{...}}

Lets define the syntax and semantics of simple types:

> data Type : Set where
>   _⇒_ : (τ₁ τ₂ : Type) → Type
>
> ⟦_⟧Type : Type → Set
> ⟦ τ₁ ⇒ τ₂ ⟧Type = ⟦ τ₁ ⟧Type → ⟦ τ₂ ⟧Type
>
> meaningOfTypes : Meaning Type
> meaningOfTypes = meaning Set ⟦_⟧Type

(Continue reading)

Andrea Vezzosi | 12 May 2013 12:00
Picon
Gravatar

Implementation of abstract vs. irrelevance

Hi,

I've noticed some very promising speedups by making definitions abstract in addition to irrelevant and I'd like to understand why.

Skimming the code I couldn't figure out where the main pieces of the implementation of these features are, is there a commentary on how they are implemented? And what work does abstract save on top of irrelevance?


Thanks,
   Andrea

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Hongseok Yang | 11 May 2013 23:35
Picon

Call for talk proposals: HOPE'13 (Workshop on Higher-Order Programming with Effects, affiliated with ICFP'13)

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

                    CALL FOR TALK PROPOSALS

                           HOPE 2013

                The 2nd ACM SIGPLAN Workshop on
              Higher-Order Programming with Effects

                       September 28, 2013
                      Boston, Massachusetts
                   (the day after ICFP 2013)

                  http://hope2013.mpi-sws.org

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

HOPE 2013 aims at bringing together researchers interested in the design, 
semantics, implementation, and verification of higher-order effectful 
programs. It will be *informal*, consisting of invited talks, contributed 
talks on work in progress, and open-ended discussion sessions. 


---------------------
Goals of the Workshop
---------------------

A recurring theme in many papers at ICFP, and in the research of many
ICFP attendees, is the interaction of higher-order programming with
various kinds of effects: storage effects, I/O, control effects,
concurrency, etc. While effects are of critical importance in many
applications, they also make it hard to build, maintain, and reason
about one's code. Higher-order languages (both functional and
object-oriented) provide a variety of abstraction mechanisms to help
"tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types,
typestate, first-class events, transactions, Hoare Type Theory,
session types, substructural and region-based type systems), and a
number of different semantic models and verification technologies have
been developed in order to codify and exploit the benefits of this
encapsulation (e.g. bisimulations, step-indexed Kripke logical
relations, higher-order separation logic, game semantics, various
modal logics). But there remain many open problems, and the field is
highly active.

The goal of the HOPE workshop is to bring researchers from a variety
of different backgrounds and perspectives together to exchange new and
exciting ideas concerning the design, semantics, implementation, and
verification of higher-order effectful programs.

We want HOPE to be as informal and interactive as possible. The
program will thus involve a combination of invited talks, contributed
talks about work in progress, and open-ended discussion
sessions. There will be no published proceedings, but participants
will be invited to submit working documents, talk slides, etc. to be
posted on this website.


-----------------------
Call for Talk Proposals
-----------------------

We solicit proposals for contributed talks. Proposals should be at
most 2 pages, in either plain text or PDF format, and should specify
how long a talk the speaker wishes to give. By default, contributed
talks will be 30 minutes long, but proposals for shorter or longer
talks will also be considered. Speakers may also submit supplementary
material (e.g. a full paper, talk slides) if they desire, which PC
members are free (but not expected) to read.

We are interested in talks on all topics related to the interaction of
higher-order programming and computational effects. Talks about work
in progress are particularly encouraged. If you have any questions
about the relevance of a particular topic, please contact the PC
chairs at the address hope2013 AT mpi-sws.org.

Deadline for talk proposals: June 14, 2013 (Friday)

Notification of acceptance:   July 28, 2013 (Sunday)

Workshop:     September 28, 2013 (Saturday)

The submission website is now open:



---------------------
Workshop Organization
---------------------

Program Co-Chairs:

Derek Dreyer (MPI-SWS, Germany)
Hongseok Yang (University of Oxford)


Program Committee:

Anindya Banerjee (IMDEA Software Institute)
Lars Birkedal (Aarhus University)
Aquinas Hobor (National University of Singapore)
Chung-Kil Hur (Microsoft Research Cambridge)
Patricia Johann (Appalachian State University)
Matthew Might (University of Utah)
Peter Mueller (ETH Zurich)
Brigitte Pientka (McGill University)
Zhong Shao (Yale)

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda

Gmane