You can subscribe to this list here.
2007 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(73) 
_{Sep}
(57) 
_{Oct}
(138) 
_{Nov}
(91) 
_{Dec}
(99) 

2008 
_{Jan}
(91) 
_{Feb}
(53) 
_{Mar}
(37) 
_{Apr}
(125) 
_{May}
(176) 
_{Jun}
(23) 
_{Jul}
(135) 
_{Aug}
(119) 
_{Sep}
(26) 
_{Oct}
(38) 
_{Nov}
(46) 
_{Dec}
(11) 
2009 
_{Jan}
(4) 
_{Feb}
(2) 
_{Mar}
(5) 
_{Apr}
(15) 
_{May}
(4) 
_{Jun}
(18) 
_{Jul}
(1) 
_{Aug}
(4) 
_{Sep}
(17) 
_{Oct}
(9) 
_{Nov}
(14) 
_{Dec}
(11) 
2010 
_{Jan}
(9) 
_{Feb}
(6) 
_{Mar}
(1) 
_{Apr}
(1) 
_{May}
(4) 
_{Jun}
(3) 
_{Jul}

_{Aug}
(10) 
_{Sep}
(7) 
_{Oct}
(7) 
_{Nov}
(36) 
_{Dec}
(23) 
2011 
_{Jan}
(2) 
_{Feb}
(1) 
_{Mar}
(1) 
_{Apr}
(11) 
_{May}
(5) 
_{Jun}
(17) 
_{Jul}
(2) 
_{Aug}
(26) 
_{Sep}
(14) 
_{Oct}
(51) 
_{Nov}
(39) 
_{Dec}
(7) 
2012 
_{Jan}
(24) 
_{Feb}
(7) 
_{Mar}
(9) 
_{Apr}
(2) 
_{May}
(9) 
_{Jun}
(7) 
_{Jul}
(3) 
_{Aug}
(1) 
_{Sep}
(8) 
_{Oct}
(12) 
_{Nov}
(1) 
_{Dec}

2013 
_{Jan}

_{Feb}

_{Mar}

_{Apr}
(35) 
_{May}
(28) 
_{Jun}
(14) 
_{Jul}
(10) 
_{Aug}
(3) 
_{Sep}
(6) 
_{Oct}

_{Nov}
(1) 
_{Dec}

2014 
_{Jan}

_{Feb}

_{Mar}

_{Apr}
(4) 
_{May}
(3) 
_{Jun}
(2) 
_{Jul}
(2) 
_{Aug}
(2) 
_{Sep}
(1) 
_{Oct}
(3) 
_{Nov}
(5) 
_{Dec}
(8) 
2015 
_{Jan}
(3) 
_{Feb}
(2) 
_{Mar}

_{Apr}

_{May}
(1) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 




1

2

3

4

5

6

7
(1) 
8

9

10

11

12

13

14
(2) 
15

16

17

18
(1) 
19

20

21
(2) 
22
(1) 
23

24

25

26

27

28

29




From: Gabriel Dos Reis <gdr@cs...>  20120222 14:33:00

Bill Page <bill.page@...> writes:  On Feb 21, 2012 12:33 PM, "Gabriel Dos Reis" <gdr@...> wrote:  >  > Bill Page <bill.page@...> writes:  >  >  I think your comment is very appropriate. Since the semantics of  >  Record is well represented as a limit (and dually, Union is  >  represented as a colimit), selecting a field is just projection (or  >  injection in the case of Union). Axiom should respect this by have  >  Record (and Union) export these operations.  >  > I am having hard time understanding what exactly you are saying. Could  > you elaborate?  >   Yes but please ask a more specific question. I thought I did. I do understand the entire paragraph.  >  It seems to me that the Axiom developers were ambivalent about the use  >  of elt (dot), apply, eval and function application. There use could be  >  simplified and clarified.  >  > The canonical operator name for `function application' is `elt' in all  > AXIOMs and that is what the axiom compilers and interpreters understand.  > `eval' isn't application; it is evaluation which is a different notion.  > All the rest is just user confusion :)  >   Does Mapping export 'eval' ? Nope.  Check the library for an example of 'apply'. that is part of "user confusion".  (Or perhaps OpenAxiom has eliminated this?) Nope.  Gaby 
From: Gabriel Dos Reis <gdr@cs...>  20120221 17:33:17

Bill Page <bill.page@...> writes:  I think your comment is very appropriate. Since the semantics of  Record is well represented as a limit (and dually, Union is  represented as a colimit), selecting a field is just projection (or  injection in the case of Union). Axiom should respect this by have  Record (and Union) export these operations. I am having hard time understanding what exactly you are saying. Could you elaborate?  It seems to me that the Axiom developers were ambivalent about the use  of elt (dot), apply, eval and function application. There use could be  simplified and clarified. The canonical operator name for `function application' is `elt' in all AXIOMs and that is what the axiom compilers and interpreters understand. `eval' isn't application; it is evaluation which is a different notion. All the rest is just user confusion :)  Gaby 
From: Gabriel Dos Reis <gdr@cs...>  20120221 16:40:32

"Serge D. Mechveliani" <mechvel@...> writes:  On Tue, Feb 14, 2012 at 02:54:17AM 0600, Gabriel Dos Reis wrote:  > "Serge D. Mechveliani" <mechvel@...> writes:  >  >  In Spad, rc.foo  >   >  selects a field named foo in a record rc.  >  In Haskell, this is  >  foo rc  similar as applying any function.  >   >  Indeed, foo has type Record(foo : Foo, ...) > Foo.  >  In particular, it allows, for example,  >  map foo (records :: List Record(...)).  >  > Haskell does not really have first class records, Haskell' folks are  > agonizing over how to properly define records in Haskell and what to do  > with the dot notation. See the various record and dot proposals and  > ongoing discussion on Haskell' list.  >  > http://hackage.haskell.org/trac/ghc/wiki/Records/DotOperator  > [..]    1. I think, it has quite good records. For example,     data Gauss r = Gauss {real :: r, im :: r}   a record    '::' means ':' of Spad.   `r' a parameter, which can be viewed as say IntegralDomain.   testL = [g, g {im = 2}, g {im = 3}]  a list of three "Gnumbers"  where  g = Gauss {real = 0, im = 1} :: Gauss Int     Then: (im (head testL)) + 3 > 4,  map im testL > [1, 2, 3]   Why do you say that it does not really have first class records? because, all the above lets you do is to name a particular field of a particular data type. It does not allow you to use the same name for the field of a completely different data type.  2. As I understand, the current Haskel discussion on records is of  _how to develop the denotations further_, to an even better state.  Because the Haskell conflict is only between good and even better :) I think that misses the fundamental point of the current discussion in the Haskell community.   For example, the next problem is the field name overloading.  For example, how to allow 'im' to appear in different records, and its  type to be found correctly. Inventing various kinds of a sugar.  I never followed the whole discussion.  But in principle, g.im still can be converted by the compiler to (im g),  there are possible various denotations.   My aim was only to point at the idea. I understood that. I was just pointing out that Spad's situation is a bit ahead of that of Haskell on this specific point.  Gaby 
From: Gabriel Dos Reis <gdr@cs...>  20120218 01:38:47

CICM 2012  Conference on Intelligent Computer Mathematics July 913, 2012 at Jacobs University, Bremen, Germany http://www.informatik.unibremen.de/cicm2012/ Call for Papers  As computers and communications technology advance, greater opportunities arise for intelligent mathematical computation. While computer algebra, automated deduction, mathematical publishing and novel user interfaces individually have long and successful histories, we are now seeing increasing opportunities for synergy among these areas. The Conference on Intelligent Computer Mathematics offers a venue for discussing these areas and their synergy. The conference will be organized by Serge Autexier and Michael Kohlhase at Jacobs University in Bremen and consist of five tracks: Artificial Intelligence and Symbolic Computation (AISC) CoChairs: John A. Campbell, Jacques Carette Calculemus Chair: Gabriel Dos Reis Digital Mathematical Libraries (DML) Chair: Petr Sojka Mathematical Knowledge Management (MKM) Chair: Makarius Wenzel Systems and Projects Chair: Volker Sorge The overall programme will be organized by the General Program Chair Johan Jeuring. Invited talks will be given by: Yannis Haralambous, Département Informatique, Télécom Bretagne Conor McBride, Department of Computer and Information Sciences, University of Strathclyde Cezar Ionescu, Potsdam Institute for Climate Impact Research  Important dates  Abstract submission: 20 February 2012 Submission deadline: 26 February 2012 Reviews sent to authors: 23 March 2012 Rebuttals due: 30 March 2012 Notification of acceptance: 6 April 2012 Camera ready copies due: 20 April 2012 Conference: 913 July 2012  Tracks  *** AISC *** Symbolic computation can be roughly described as the study of algorithms which operate on expression trees. Another way to phrase this is to say that the denotational semantics of expressions trees is not fixed, but is rather context dependent. Expression simplification is probably the archetypal symbolic computation. Mathematically oriented software (such as the socalled computer algebra systems) have been doing this for decades, but not long thereafter, systems doing proof planning and theorem discovery also started doing the same; some attempts at knowledge management and 'expert systems' were also symbolic, but less successfully so. More recently, many different kinds of program analyses have gotten `symbolic', as well as some of the automated theorem proving (SMT, CAV, etc). But a large number of the underlying problems solved by symbolic techniques are well known to be undecidable (never mind the many that are EXPtime complete, etc). Artificial Intelligence has been attacking many of these different subproblems for quite some time, and has also built up a solid body of knowledge. In fact, most symbolic computation systems grew out of AI projects. These two fields definitely intersect. One could say that in the intersection lies all those problems for which we have no decision procedures. In other words, decision procedures mark a definite phase shift in our understanding, but are not always possible. Yet we still want to solve certain problems, and must find 'other' means of (partial) solution. This is the fertile land which comprises the core of AISC. Rather than try to exhaustively list topics of interest, it is simplest to say that AISC seeks work which advances the understanding of Solving problems which fundamentally involve the manipulation of expressions, but for which decision procedures are unlikely to ever exist. *** Calculemus *** Calculemus is a series of conferences dedicated to the integration of computer algebra systems (CAS) and systems for mechanised reasoning, the interactive theorem provers or proof assistants (PA) and the automated theorem provers (ATP). Currently, symbolic computation is divided into several (more or less) independent branches: traditional ones (e.g., computer algebra and mechanised reasoning) as well as newly emerging ones (on user interfaces, knowledge management, theory exploration, etc.) The main concern of the Calculemus community is to bring these developments together in order to facilitate the theory, design, and implementation of integrated systems for computer mathematics that will routinely be used by mathematicians, computer scientists and engineers in their every day business. The topics of interest of Calculemus include but are not limited to: * Theorem proving in computer algebra (CAS) * Computer algebra in theorem proving (PA and ATP) * Case studies and applications that both involve computer algebra and mechanised reasoning * Representation of mathematics in computer algebra * Adding computational capabilities to PA and ATP * Formal methods requiring mixed computing and proving * Combining methods of symbolic computation and formal deduction * Mathematical computation in PA and ATP * Theory, design and implementation of interdisciplinary systems for computer mathematics * Theory exploration techniques * Input languages, programming languages, types and constraint languages, and modeling languages for mechanised mathematics systems (PA, CAS, and ATP). * Infrastructure for mathematical services *** DML *** Mathematicians dream of a digital archive containing all peerreviewed mathematical literature ever published, properly linked, validated and verified. It is estimated that the entire corpus of mathematical knowledge published over the centuries does not exceed 100,000,000 pages, an amount easily manageable by current information technologies. Following success of DML 2008, DML 2009 DML 2010, and DML 2011 track objectives are to formulate the strategy and goals of a global mathematical digital library and to summarize the current successes and failures of ongoing technologies and related projects as EuDML, asking such questions as: * What technologies, standards, algorithms and formats should be used and what metadata should be shared? * What business models are suitable for publishers of mathematical literature, authors and funders of their projects and institutions? * Is there a model of sustainable, interoperable, and extensible mathematical library that mathematicians can use in their everyday work? * What is the best practice for * retrodigitized mathematics (from images via OCR to MathML or TeX); * retroborndigital mathematics (from existing electronic copy in DVI, PS or PDF to MathML or TeX); * borndigital mathematics (how to make needed metadata and file formats available as a side effect of publishing workflow [CEDRAM/Euclid model])? DML is an opportunity to share experience and best practices between projects in any area (MKM, NLP, OCR, pattern recognition, whatever) that could change the paradigm for searching, accessing, and interacting with the mathematical corpus. The track is trans/interdisciplinary and contributions from any kind of people on any aspect of the DML building are welcome. *** MKM *** Mathematical Knowledge Management is an interdisciplinary field of research in the intersection of mathematics, computer science, library science, and scientific publishing. The objective of MKM is to develop new and better ways of managing sophisticated mathematical knowledge, based on innovative technology of computer science, the Internet, and intelligent knowledge processing. MKM is expected to serve mathematicians, scientists, and engineers who produce and use mathematical knowledge; educators and students who teach and learn mathematics; publishers who offer mathematical textbooks and disseminate new mathematical results; and librarians and mathematicians who catalog and organize mathematical knowledge. The conference is concerned with all aspects of mathematical knowledge management. A nonexclusive list of important topics includes: * Representations of mathematical knowledge * Authoring languages and tools * Repositories of formalized mathematics * Deduction systems * Mathematical digital libraries * Diagrammatic representations * Mathematical OCR * Mathematical search and retrieval * Math assistants, tutoring and assessment systems * MathML, OpenMath, and other mathematical content standards * Web presentation of mathematics * Data mining, discovery, theory exploration * Computer algebra systems * Collaboration tools for mathematics * Challenges and solutions for mathematical workflows *** Systems and Projects *** The Systems and Projects track of the Conferences on Intelligent Computer Mathematics is a forum for presentation of systems and new and ongoing projects in all areas and topics related to the CICM conferences: * AI and Symbolic Computation * Deduction and Computer Algebra * Mathematical Knowledge Management * Digital Mathematical Libraries The track aims to provide an overview of the latest developments and trends within the CICM community as well as to exchange ideas between developers and introduce systems to an audience of potential users. We solicit submissions for two page abstracts in the categories of system descriptions and project presentations. System description should present * newly developed systems, * systems that have not previously been presented to the CICM community, or * significant updates to existing systems. Project presentation should describe * projects that are new or about to start, * ongoing projects that have not yet been presented to the CICM community. * significant new developments in ongoing previously presented projects. All submissions should contain links to demos, downloadable systems, or project pages. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted abstracts will be published in the CICM proceedings in Springer's LNAI series. Author's are expected to present their abstracts in 510 minute teaser talks followed by an open demo/poster session. System papers must be accompanied by a system demonstration, while project papers must be accompanied by a poster presentation.  Submitting  Submissions to tracks A to D must not exceed 15 pages and will be reviewed and evaluated with respect to relevance, clarity, quality, originality, and impact. Shorter papers, e.g., for system descriptions, are welcome. Authors will have an opportunity to respond to their papers' reviews before the programme committee makes a decision. Submissions to the Systems & Projects track must not exceed four pages. The accepted abstracts will be presented at CICM in a fast presentation session, followed by an open demo/poster session. System papers must be accompanied by a system demonstration, and project papers must be accompanied by a poster presentation. The four pages of the abstract should be new material, accompanied by links to demos/downloads/projectpages and [existing] system descriptions. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted conference submissions from all tracks will be published as a volume in the series Lecture Notes in Artificial Intelligence (LNAI) by Springer. In addition to these formal proceedings, authors are permitted and encouraged to publish the final versions of their papers on arXiv.org. Workinprogress submissions are intended to provide a forum for the presentation of original work that is not (yet) in a suitable form for submission as a full or system description paper. This includes work in progress and emerging trends. Their size is not limited, but we recommend 5  10 pages. The programme committee may offer authors of rejected formal submissions to publish their contributions as workinprogress papers instead. Depending on the number of workinprogress papers accepted, they will be presented at the conference either as short talks or as posters. The workinprogress proceedings will be published as a technical report. All papers should be prepared in LaTeX and formatted according to the requirements of Springer's LNCS series (the corresponding style files can be downloaded from http://www.springer.de/comp/lncs/authors.html). By submitting a paper the authors agree that if it is accepted at least one of the authors will attend the conference to present it. Electronic submission is done through easychair (http://www.easychair.org/conferences/?conf=cicm2012).  Program Committees  General chair: Johan Jeuring (Utrecht University and Open Universiteit the Netherlands) AISC track John A. Campbell; University College London, UK; Cochair Jacques Carette; McMaster University, Canada; Cochair Serge Autexier; DFKI Bremen, Germany Jacques Calmet; University of Karlsruhe, Germany Jacques Fleuriot; University of Edinburgh, UK Andrea Kohlhase; International University Bremen, Germany Erik Postma; Maplesoft Inc., Canada Alan Sexton; University of Birmingham, UK Chungchieh Shan; Cornell University, USA. Stephen Watt; University of Western Ontario, Canada Calculemus track Gabriel Dos Reis; Texas A&M University, USA; Chair Andrea Asperti; University of Bologna, Italy Laurent Bernardin; Maplesoft, Canada James Davenport; University of Bath, UK Ruben Gamboa; University of Wyoming, USA Mark Giesbrecht; University of Waterloo, Canada Sumit Gulwani; Microsoft Research, USA John Harrison; Intel, USA Joris van der Hoeven; École Polytechnique, France Hoon Hong; North Carolina State University, USA Loïc Pottier; INRIA, France Wolfgang Windsteiger; RISC, Austria DML track Petr Sojka; Masaryk University, Brno, CZ; Chair José Borbinha; Technical University of Lisbon, PT Thierry Bouche; University Grenoble, FR Michael Doob; University of Manitoba, Winnipeg, CA Thomas Fischer; Goettingen University, DE Yannis Haralambous; Télécom Bretagne, FR Václav Hlaváč; Czech Technical University, Prague, CZ Michael Kohlhase; Jacobs University Bremen, DE Janka Chlebíková; Portsmouth University, UK Enrique MaciásVirgós; University of Santiago de Compostela, ES Bruce Miller; NIST, USA Jiří Rákosník; Academy of Sciences, Prague, CZ Eugenio Rocha; University of Aveiro, PT David Ruddy; Cornell University, US Volker Sorge; University of Birmingham, UK Masakazu Suzuki; Kyushu University, JP MKM track Makarius Wenzel; University of ParisSouth, France; Chair David Aspinall; University of Edinburgh, Scotland Jeremy Avigad; Carnegie Mellon University, USA Mateja Jamnik; University of Cambridge, UK Cezary Kaliszyk; University of Tsukuba, Japan Manfred Kerber; University of Birmingham, UK Christoph Lüth; DFKI Bremen, Germany Adam Naumowicz; University of Białystok, Poland Jim Pitman; University of California, Berkeley, USA Pedro Quaresma; Universidade de Coimbra, Portugal Florian Rabe; Jacobs University Bremen, Germany Claudio Sacerdoti Coen; University of Bologna, Italy Enrico Tassi; INRIA Saclay, France Freek Wiedijk; Radboud University Nijmegen, The Netherlands Systems & Projects track Volker Sorge; University of Birmingham, UK; Chair Josef Baker; University of Birmingham, UK John Charnley; Imperial College, UK Manuel Kauers; RISC, Austria Koji Nakagawa; Kyushu University, Japan Piotr Rudnicki; University of Alberta, Canada Josef Urban; Radboud University Nijmegen, The Netherlands Richard Zanibbi; Rochester Institute of Technologies, USA 
From: Gabriel Dos Reis <gdr@cs...>  20120214 09:08:59

"Serge D. Mechveliani" <mechvel@...> writes:  Another note on the Spad language:  for a record  Foo(coef: Integer, exp: Integer, root: Integer),  its setting syntax by [1, 3, 2] :: Foo  is a bug farm.  Is not it?  The syntax like [coef := 1, exp := 3, root := 2] the suggested syntax already has a valid meaning: it sets three variables and return a List Integer. It does not look like a better alternative to the current syntax.   (replace `:=' with something appropriate)  is much more safe. And here the named fieds can be transposed, the  programmer will not need to remember the order of, say, 6 fields.   Regards,     Sergei  mechvel@... 
From: Gabriel Dos Reis <gdr@cs...>  20120214 08:54:29

"Serge D. Mechveliani" <mechvel@...> writes:  In Spad, rc.foo   selects a field named foo in a record rc.  In Haskell, this is  foo rc  similar as applying any function.   Indeed, foo has type Record(foo : Foo, ...) > Foo.  In particular, it allows, for example,  map foo (records :: List Record(...)). Haskell does not really have first class records, Haskell' folks are agonizing over how to properly define records in Haskell and what to do with the dot notation. See the various record and dot proposals and ongoing discussion on Haskell' list. http://hackage.haskell.org/trac/ghc/wiki/Records/DotOperator http://www.haskell.org/pipermail/haskellprime/2012February/003515.html http://www.haskell.org/haskellwiki/TypeDirectedNameResolution http://hackage.haskell.org/trac/haskellprime/wiki/TypeDirectedNameResolution  Gaby 
From: Gabriel Dos Reis <gdr@cs...>  20120207 09:35:02

Waldek Hebisch <hebisch@...> writes:  Serge D. Mechveliani wrote:  >  > On Sun, Feb 05, 2012 at 01:56:20AM +0100, Ralf Hemmecke wrote:  > > On 02/04/2012 06:13 PM, Serge D. Mechveliani wrote:  > >> [..]  > >>>> dropWhile(p: Character > Boolean, xs: List Character) :  > >>>> List Character ==  > >>>> empty? xs => xs  > >>>> p first(xs) => dropWhile(p, rest xs)  > >>>> xs  > >>>> Is this more efficient? [...]  Spad compiler will inline "simple enough" functions. Unfortunately,  currently this means functions consisting of single operation.   Your version will generate the following Lisp code:   (DEFUN TTT;dropWhile;M2L;1 (p xs $)  (COND ((OR (NULL xs) (NULL (SPADCALL (SPADfirst xs) p))) xs)  ('T (SPADCALL p (CDR xs) (QREFELT $ 8))))) OpenAxiom resolves these SPADCALLs within the same package/domain and produces (DEFUN SERGEI;dropWhile;M2L;1 (p xs $) (COND ((OR (NULL xs) (NOT (SPADCALL (SPADfirst xs) p))) xs) (T (SERGEI;dropWhile;M2L;1 p (CDR xs) $)))) which any of the free Lisp supported by OpenAxiom is capable of recognizing as tailrecursive, and therefore optimize appropriately.  Gaby 