Author: deadalnix
Revision Date: 2018-05-26 14:40:42 UTC

Fix comment decribing setcccarry. NFC

Author: imath
Revision Date: 2018-05-26 12:47:08 UTC

Messages UI: Create a new Backbone view to wrap hooks caught output

This new view can be used when hooks caught output cannot be inserted into regular views. {{{bp_before_member_messages_loop}}} and {{{bp_before_member_messages_loop}}} are two good examples.

See #7850 (Trunk)

Author: SergeyBiryukov
Revision Date: 2018-05-26 12:43:23 UTC

Posts, Post Types: Clear post password cookie when logging out.

Props skoldin, subrataemfluence, ianbelanger, johnbillion.
Fixes #44089.
Built from https://develop.svn.wordpress.org/trunk@43317

Author: Simon Tatham
Revision Date: 2018-05-26 12:37:46 UTC

Enable -Wpointer-arith in the autoconf build.

That should stop me making that kind of mistake again.

Author: hjl
Revision Date: 2018-05-26 11:35:31 UTC

 Don't check ifunc_resolver on error

Since ifunc_resolver isn't set when an error is detected, we should
lookup ifunc attribute in this case.

 PR target/85900
 PR target/85345
 * varasm.c (assemble_alias): Lookup ifunc attribute on error.

Author: hjl
Revision Date: 2018-05-26 11:35:31 UTC

 Don't check ifunc_resolver on error

Since ifunc_resolver isn't set when an error is detected, we should
lookup ifunc attribute in this case.

 PR target/85900
 PR target/85345
 * varasm.c (assemble_alias): Lookup ifunc attribute on error.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@260792 138bc75d-0d04-0410-961f-82ee72b054a4

Author: Pascal Quantin
Revision Date: 2018-05-26 11:23:51 UTC

SCTP: fix crash when filtering an association

Do not free a tsn_t element if it has already been inserted in a GList.
The code structure is complex enough to add an explicit check before
calling g_free().
Fixes a regression introduced in gb19ca06fcc.

While we are at it, let's call the correct free function and plug some
memory leaks.

Bug: 14733
Change-Id: I071da96982da569083fd98b790e0d37ac0826ff1
Reviewed-on: https://code.wireshark.org/review/27808
Reviewed-by: Pascal Quantin <pascal.quantin@gmail.com>
Petri-Dish: Pascal Quantin <pascal.quantin@gmail.com>
Tested-by: Petri Dish Buildbot
Reviewed-by: Peter Wu <peter@lekensteyn.nl>

Author: trasz
Revision Date: 2018-05-26 11:13:17 UTC

Revert r333493, which was a temporary fix for 11.2-RELEASE, and instead
switch the default kldxref_enable to YES.

The reason is that it's required for every image that's being cross-built,
as kldxref(8) cannot handle files for non-native architectures. For the
one that is not - amd64 - having it on by default doesn't change anything;
the script is noop if the linker.hints already exists.

MFC after: 2 weeks
Sponsored by: DARPA, AFRL

Author: Seong-ho Cho
Revision Date: 2018-05-26 10:33:21 UTC

I18n: Update translation ko (100%).

229 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Anonymous
Revision Date: 2018-05-26 10:32:10 UTC

I18n: Update translation pl (100%).

391 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Adam Reichold
Revision Date: 2018-05-26 09:55:23 UTC

LZWStream: make inputBuf unsigned

since shifting negative numbers is undefined according to spec

Author: xbolva00
Revision Date: 2018-05-26 09:24:00 UTC

[ClangDiagnostics] Silence warning about fallthrough after PrintFatalError

Summary:
ClangDiagnosticsEmitter.cpp:1047:57: warning: this statement may fall through [-Wimplicit-fallthrough=]
       Builder.PrintFatalError("Unknown modifier type: " + Modifier);
                               ~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~
ClangDiagnosticsEmitter.cpp:1048:5: note: here
     case MT_Select: {
                   ^

Reviewers: rsmith, rtrieu

Reviewed By: rtrieu

Subscribers: rtrieu, ilya-biryukov, ioeric, MaskRay, jkorous, cfe-commits

Differential Revision: https://reviews.llvm.org/D47340

Author: Sebastian Geiger
Revision Date: 2018-05-26 06:59:07 UTC

Readme.md: convert to markdown

Author: Scott D Phillips
Revision Date: 2018-05-26 04:35:50 UTC

i965/miptree: Use cpu tiling/detiling when mapping

Rename the (un)map_gtt functions to (un)map_map (map by
returning a map) and add new functions (un)map_tiled_memcpy that
return a shadow buffer populated with the intel_tiled_memcpy
functions.

Tiling/detiling with the cpu will be the only way to handle Yf/Ys
tiling, when support is added for those formats.

v2: Compute extents properly in the x|y-rounded-down case (Chris Wilson)

v3: Add units to parameter names of tile_extents (Nanley Chery)
    Use _mesa_align_malloc for the shadow copy (Nanley)
    Continue using gtt maps on gen4 (Nanley)

v4: Use streaming_load_memcpy when detiling

v5: (edited by Ken) Move map_tiled_memcpy above map_movntdqa, so it
    takes precedence. Add intel_miptree_access_raw, needed after
    rebasing on commit b499b85b0f2cc0c82b7c9af91502c2814fdc8e67.

Reviewed-by: Chris Wilson <chris@chris-wilson.co.uk>
Reviewed-by: Kenneth Graunke <kenneth@whitecape.org>

Author: Scott D Phillips
Revision Date: 2018-05-26 04:35:50 UTC

i965/miptree: Use cpu tiling/detiling when mapping

Rename the (un)map_gtt functions to (un)map_map (map by
returning a map) and add new functions (un)map_tiled_memcpy that
return a shadow buffer populated with the intel_tiled_memcpy
functions.

Tiling/detiling with the cpu will be the only way to handle Yf/Ys
tiling, when support is added for those formats.

v2: Compute extents properly in the x|y-rounded-down case (Chris Wilson)

v3: Add units to parameter names of tile_extents (Nanley Chery)
    Use _mesa_align_malloc for the shadow copy (Nanley)
    Continue using gtt maps on gen4 (Nanley)

v4: Use streaming_load_memcpy when detiling

v5: (edited by Ken) Move map_tiled_memcpy above map_movntdqa, so it
    takes precedence. Add intel_miptree_access_raw, needed after
    rebasing on commit b499b85b0f2cc0c82b7c9af91502c2814fdc8e67.

Reviewed-by: Chris Wilson <chris@chris-wilson.co.uk>
Reviewed-by: Kenneth Graunke <kenneth@whitecape.org>

Author: Morten Welinder
Revision Date: 2018-05-26 03:04:32 UTC

GnmFunc: patch up things to please the test suite.

(I.e., things didn't work and crashes left and right. That sort of thing.)

Author: Michael Niedermayer
Revision Date: 2018-05-25 22:54:55 UTC

avcodec/mlpdec: Only change noise_type if the related fields are valid

Fixes: inconsistency
Fixes:runtime error: index 8 out of bounds for type 'int32_t [8]'
Fixes: 6686/clusterfuzz-testcase-minimized-ffmpeg_AV_CODEC_ID_TRUEHD_fuzzer-5191383498358784

Found-by: continuous fuzzing process https://github.com/google/oss-fuzz/tree/master/projects/ffmpeg
Signed-off-by: Michael Niedermayer <michael@niedermayer.cc>

Author: Alexandre Julliard
Revision Date: 2018-05-25 18:38:57 UTC

Release 3.9.

Signed-off-by: Alexandre Julliard <julliard@winehq.org>

Author: Tom Lane
Revision Date: 2018-05-25 18:31:06 UTC

Fix misidentification of SQL statement type in plpgsql's exec_stmt_execsql.

To distinguish SQL statements that are INSERT/UPDATE/DELETE from other
ones, exec_stmt_execsql looked at the post-rewrite form of the statement
rather than the original. This is problematic because it did that only
during first execution of the statement (in a session), but the correct
answer could change later due to addition or removal of DO INSTEAD rules
during the session. That could lead to an Assert failure, as reported
by Tushar Ahuja and Robert Haas. In non-assert builds, there's a hazard
that we would fail to enforce STRICT behavior when we'd be expected to.
That would happen if an initially present DO INSTEAD, that replaced the
original statement with one of a different type, were removed; after that
the statement should act "normally", including strictness enforcement, but
it didn't. (The converse case of enforcing strictness when we shouldn't
doesn't seem to be a hazard, as addition of a DO INSTEAD that changes the
statement type would always lead to acting as though the statement returned
zero rows, so that the strictness error could not fire.)

To fix, inspect the original form of the statement not the post-rewrite
form, making it valid to assume the answer can't change intra-session.
This should lead to the same answer in every case except when there is a
DO INSTEAD that changes the statement type; we will now set mod_stmt=true
anyway, while we would not have done so before. That breaks the Assert
in the SPI_OK_REWRITTEN code path, which expected the latter behavior.
It might be all right to assert mod_stmt rather than !mod_stmt there,
but I'm not entirely convinced that that'd always hold, so just remove
the assertion altogether.

This has been broken for a long time, so back-patch to all supported
branches.

Discussion: https://postgr.es/m/CA+TgmoZUrRN4xvZe_BbBn_Xp0BDwuMEue-0OyF0fJpfvU2Yc7Q@mail.gmail.com

Author: Benno Schulenberg
Revision Date: 2018-05-25 18:09:24 UTC

tweaks: rename a function, for more aptness and extra contrast

Author: Mike Fleetwood
Revision Date: 2018-05-25 16:18:49 UTC

Add logo.png for automatic GitLab/GitHub project avatar

Generated from GParted SVG icon using:
    rsvg -w 256 -h 256 data/icons/hicolor_apps_scalable_gparted.svg logo.png

Author: Vda-linux
Revision Date: 2018-05-25 15:03:46 UTC

unlzma: close another SEGV possibility

function old new delta
unpack_lzma_stream 2669 2686 +17

Signed-off-by: Denys Vlasenko <vda.linux@googlemail.com>

Author: Morten Welinder
Revision Date: 2018-05-25 13:33:16 UTC

Debug improvement

Author: Jun-ichi Takimoto
Revision Date: 2018-05-25 12:11:20 UTC

42809: slightly improve 'compset -q'

Author: Szymon Janc
Revision Date: 2018-05-25 12:06:17 UTC

android: Fix some compilation warnings

Author: wouter
Revision Date: 2018-05-25 10:41:24 UTC

- Fix close events for tcp only.

Author: Clément DAVID
Revision Date: 2018-05-25 08:11:37 UTC

Merge 6.0 into master

Change-Id: I3322fcacba486acd90851cabad646b52c1d0e7b5

Author: dormando
Revision Date: 2018-05-25 06:57:03 UTC

fix sasl tests

apparently I broke them with the unix domain socket update, since you have to
add an environment variable for them to even run.

need to make it work with the unix socket at some point though.

Author: Arnold Robbins
Revision Date: 2018-05-25 06:56:44 UTC

Sync the Italian translation.

Author: Akira TAGOH
Revision Date: 2018-05-25 06:24:44 UTC

Add a test case for bz#106618

Author: Christian Hammond
Revision Date: 2018-05-25 02:51:01 UTC

Merge branch 'release-4.0.x'

Author: Steve Markgraf
Revision Date: 2018-05-24 22:16:38 UTC

tuner_r82xx: turn off loop-through, remove dead code

As pointed out by Carl Laufer on the mailing list,
turning the loop-through output off reduces the
current consumption by 10-20mA which in turn reduces
the heat a bit. So far there seem to be no devices
that have anything connected to the loop-through output.

Signed-off-by: Steve Markgraf <steve@steve-m.de>

Author: Wolfgang Dautermann
Revision Date: 2018-05-24 19:47:32 UTC

Travis: Update CMake

Author: Rex Dieter
Revision Date: 2018-05-24 19:40:53 UTC

xdg-open: better pcmanfm check (BR106636,BR106161)

Author: Howard Chu
Revision Date: 2018-05-24 16:53:10 UTC

ITS#8616 don't check for existing value when deleting values

Author: k0kubun
Revision Date: 2018-05-24 14:32:05 UTC

spec/ruby: fix RUBY_DESCRIPTION check with JIT enabled

`make test-spec` adds `-r./$(arch)-fake` to pass header options.
But the $(arch)-fake.rb unexpectedly modifies RUBY_DESCRIPTION and it
always drops +JIT from it since the fake.rb is built with BOOTSTRAPRUBY,
which can be miniruby. miniruby can't find MJIT header and thus
mjit_init_p is always FALSE.

So, to pass `make test-spec` with JIT enabled, we can't use
RUBY_DESCRIPTION.

Author: Tobias Brunner
Revision Date: 2018-05-24 10:18:18 UTC

NEWS: Some minor updates

Author: Ben Elliston
Revision Date: 2018-05-24 08:25:10 UTC

 * testsuite/config-sub.data: Add tests for Sequent and DYNIX/ptx.

Author: christos
Revision Date: 2018-05-24 00:27:24 UTC

Since ${MAKE} converts $$ -> $ during parsing we need to put it back to
preserve the original variable value with :Q.
XXX: pullup-8

Author: Nuno Miguel
Revision Date: 2018-05-23 16:30:24 UTC

I18n: Update translation pt (100%).

744 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Matthias Sohn
Revision Date: 2018-05-23 15:25:49 UTC

Prepare 5.1.0-SNAPSHOT builds

Change-Id: I5b4427a73f05ed2144d886acb37640fc714757bc
Signed-off-by: Matthias Sohn <matthias.sohn@sap.com>

Author: Julian Scheel
Revision Date: 2018-05-23 14:06:07 UTC

speaker-test: Remove unused variable

Signed-off-by: Julian Scheel <julian@jusst.de>
Signed-off-by: Takashi Iwai <tiwai@suse.de>

Author: Matthias Sohn
Revision Date: 2018-05-23 08:18:18 UTC

Prepare 5.1.0-SNAPSHOT builds

Change-Id: I8523a993ae1f7b62573d7547273bc1356bf64fa7
Signed-off-by: Matthias Sohn <matthias.sohn@sap.com>

Author: Michel Dänzer
Revision Date: 2018-05-22 16:30:48 UTC

glamor: Bail CreatePixmap on unsupported pixmap depth

Fixes crash in that case.

Bugzilla: https://bugs.freedesktop.org/106293
Reviewed-by: Alex Deucher <alexander.deucher@amd.com>

Author: Piotr Drąg
Revision Date: 2018-05-22 16:29:52 UTC

Update Polish translation

Author: Takashi Iwai
Revision Date: 2018-05-22 12:17:41 UTC

usb_stream: Add explicit -lpthread to *_LIBADD

The pthread library has to be linked for this module. In some tool
chains, it results in a build error.

Signed-off-by: Takashi Iwai <tiwai@suse.de>

Author: Clement Lefebvre
Revision Date: 2018-05-22 10:16:57 UTC

5.3.5

Author: Rico Tzschichholz
Revision Date: 2018-05-22 07:42:49 UTC

webkit2gtk-4.0: Update to 2.21.2

Author: Daniel Williams
Revision Date: 2018-05-22 00:35:05 UTC

[PATCH] [fix] gps/*py now passes `scons check`

Whoops, the auto reconnect patch broke scons check.

Signed-off-by: Gary E. Miller <gem@rellim.com>

Author: David Robillard
Revision Date: 2018-05-21 08:35:36 UTC

Clarify time:beat origin

Author: Milan Crha
Revision Date: 2018-05-21 08:01:29 UTC

Post-release version bump

Author: Carlos Puchol
Revision Date: 2018-05-19 00:06:45 UTC

update older lock files

Author: Richard Shann
Revision Date: 2018-05-18 14:08:51 UTC

Fix bug #53937: midi input does not shut off

Author: vboxsync
Revision Date: 2018-05-18 10:22:17 UTC

testboxscript: introduce a way to specify custom mount options

Author: Michael Martins
Revision Date: 2018-05-17 04:33:23 UTC

I18n: Update translation pt_BR (100%).

169 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Michael Martins
Revision Date: 2018-05-17 04:31:18 UTC

I18n: Update translation pt_BR (100%).

209 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Clement Lefebvre
Revision Date: 2018-05-16 12:50:35 UTC

18.04.1+linuxmint4

Author: daly
Revision Date: 2018-05-16 07:09:17 UTC

books/bookvolbib add references

Goal: Proving Axiom Correct

\index{Walther, J.S.}
\begin{chunk}{axiom.bib}
@misc{Walt71,
  author = "Walther, J.S.",
  title = {{A Unified Algorithm for Elementary Functions}},
  link = "\url{}",
  year = "1971",
  abstract =
    "This paper describes a single unified algorithm for the calculation
    of elementary functions including multipli- cation, division, sin,
    cos, tan, arctan, sinh, cosh, tanh, arctanh, In, exp and square-root.
    The basis for the algorithm is coordinate rotation in a linear,
    circular, or hyperbolic coordinate system depending on which function
    is to be calculated. The only operations re- quired are shifting,
    adding, subtracting and the recall of prestored constants. The
    limited domain of con- vergence of the algorithm is calculated,
    leading to a discussion of the modifications required to extend the
    domain for floating point calculations.

    A hardware floating point processor using the algo- rithm was built at
    Hewlett-Packard Laboratories. The block diagram of the processor, the
    microprogram control used for the algorithm, and measures of actual
    performance are shown.",
  paper = "Walt71.pdf"
}

\end{chunk}

\index{Friedman, Daniel P.}
\index{Wise, David S.}
\begin{chunk}{axiom.bib}
@techreport{Frie76,
  author = "Friedman, Daniel P. and Wise, David S.",
  title = {{CONS should not Evaluate its Arguments}},
  institution = "Indiana University",
  number = "TR44",
  year = "1976",
  abstract =
    "The constructor function which allocates and fills records in
    recursive, side-effect-free procedural languages is redefined to be a
    non-strict (Vuillemin 1974) elementary operation. Instead of
    evaluating its arguments, it builds suspensions of them which are not
    coerced until the suspensions is accessed by strict elementary
    function. The resulting evalutation procedures are strictly more
    powerful than existing schemes for languages such as LISP. The main
    results are that Landin's streams are subsumed into McCarthy's LISP
    merely by the redefinition of elementar functions, that invocations of
    LISP's evaluator can be minimized by redefining the elemntary
    functions without redefining the interpreter, and as a strong
    conjecture, that redefining the elementary functions yields the least
    fixed-point semantics for McCarthy's evalution scheme. This new
    insight into the role of construction functions will do much to ease
    the interface between recursive programmers and iterative programmers,
    as well as the interface between programmers and data structure
    designers.",
  paper = "Frie16.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Sarma, Gopal}
\index{Hay, Nick J.}
\begin{chunk}{axiom.bib}
@article{Sarm17,
  author = "Sarma, Gopal and Hay, Nick J.",
  title = {{Robust Computer Algebra, Theorem Proving, and Oracle AI}},
  journal = "Informatica",
  volume = "41",
  number = "3",
  link = "\url{https://arxiv.org/pdf/1708.02553.pdf}",
  year = "2017",
  abstract =
    "In the context of superintelligent AI systems, the term 'oracle' has
    two meanings. One refers to modular systems queried for
    domain-specific tasks. Another usage, referring to a class of systems
    which may be useful for addressing the value alignment and AI control
    problems, is a superintelligent AI system that only answers questions.
    The aim of this manuscript is to survey contemporary research problems
    related to oracles which align with long-term research goals of AI
    safety. We examine existing question answering systems and argue that
    their high degree of architectural heterogeneity makes them poor
    candidates for rigorous analysis as oracles. On the other hand, we
    identify computer algebra systems (CASs) as being primitive examples
    of domain-specific oracles for mathematics and argue that efforts to
    integrate computer algebra systems with theorem provers, systems which
    have largely been developed independent of one another, provide a
    concrete set of problems related to the notion of provable safety that
    has emerged in the AI safety community. We review approaches to
    interfacing CASs with theorem provers, describe well-defined
    architectural deficiencies that have been identified with CASs, and
    suggest possible lines of research and practical software projects for
    scientists interested in AI safety.",
  paper = "Sarm17.pdf",
  keywords = "printed, axiomref"
}

\end{chunk}

\index{Keller, Chantal}
\begin{chunk}{axiom.bib}
@phdthesis{Kell13,
  author = "Keller, C.",
  title = {{A Matter of Trust: Skeptical Commuication Between Coq and
            External Provers}},
  school = "Ecole Polytechnique",
  year = "2013",
  link =
"\url{https://www.lri.fr/~keller/Documents-recherche/Publications/thesis13.pdf}",
  abstract =
    "This thesis studies the cooperation between the Coq proof assistant
    and external provers through proof witnesses. We concentrate on two
    different kinds of provers that can return certicates: first, answers
    coming from SAT and SMT solvers can be checked in Coq to increase both
    the confidence in these solvers and Coq 's automation; second,
    theorems established in interactive provers based on Higher-Order
    Logic can be exported to Coq and checked again, in order to offer the
    possibility to produce formal developments which mix these two
    different logical paradigms. It ended up in two software : SMTCoq, a
    bi-directional cooperation between Coq and SAT/SMT solvers, and
    HOLLIGHTCOQ, a tool importing HOL Light theorems into Coq.

    For both tools, we took great care to define a modular and efficient
    architecture, based on three clearly separated ingredients: an
    embedding of the formalism of the external tool inside Coq which is
    carefully translated into Coq terms, a certified checker to establish
    the proofs using the certicates and a Ocaml preprocessor to transform
    proof witnesses coming from different provers into a generic
    certificate. This division allows that a change in the format of proof
    witnesses only affects the preprocessor, but no proved Coq code.
    Another fundamental component for efficiency and modularity is
    computational reflection, which exploits the computational power of
    Coq to establish generic and small proofs based on the certicates.",
  paper = "Kell13.pdf"
}

\end{chunk}

\index{Farmer, William M.}
\begin{chunk}{axiom.bib}
@article{Farm07,
  author = "Farmer, William M.",
  title = {{Biform Theories in Chiron}},
  journal = "LNCS",
  volume = "4573",
  pages = "66-79",
  year = "2007",
  abstract =
    "An axiomatic theory represents mathematical knowledge declaratively
    as a set of axioms. An algorithmic theory represents mathematical
    knowledge procedurally as a set of algorithms. A biform theory is
    simultaneously an axiomatic theory and an algorithmic theory. It
    represents mathematical knowledge both declaratively and procedurally.
    Since the algorithms of algorithmic theories manipulate th e syntax of
    expressions, biform theories —- as well as algorithmic theories -— are
    difficult to formalize in a traditional logic without the means to
    reason about syntax. Chiron is a derivative of
    von-Neumann-Bernays-G̈odel ( NBG ) set theory that is intended to be a
    practical, general-purpose logic for mechanizing mathematics. It
    includes elements of type theory, a scheme for handling undefinedness,
    and a facility for reasoning about the syntax of expressions. It is an
    exceptionally well-suited logic for formalizing biform theories. This
    paper defines the notion of a biform theory, gives an overview of
    Chiron, and illustrates how biform theories can be formalized in Chiron.",
  paper = "Farm07.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Carette, Jacques}
\index{Farmer, William M.}
\index{Sorge, Volker}
\begin{chunk}{axiom.bib}
@inproceedings{Care07,
  author = "Carette, Jacques and Farmer, William M. and Sorge, Volker",
  title = {{A Rational Reconstruction of a System for Experimental
            Mathematics}},
  booktitle = "14th Workshop on Automated Reasoning",
  publisher = "unknown",
  year = "2007",
  abstract =
    "In previous papers we described the implementation of a system
    which combines mathematical object generation, transformation and
    filtering, conjecture generation, proving and disproving for
    mathematical discovery in non-associative algebra. While the system
    has generated novel, fully verified theorems, their construction
    involved a lot of ad hoc communication between disparate systems. In
    this paper we carefully reconstruct a specification of a sub-process
    of the original system in a framework for trustable communication
    between mathematics systems put forth by us. It employs the concept
    of biform theories that enables the combined formalisation of the
    axiomatic and algorithmic theories behind the generation
    process. This allows us to gain a much better understanding of the
    original system, and exposes clear generalisation opportunities.",
  paper = "Care07.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Farmer, William M.}
\begin{chunk}{axiom.bib}
@inproceedings{Farm00,
  author = "Farmer, William M.",
  title = {{A Proposal for the Development of an Interactive
            Mathematics Laboratory for Mathematics Eductions}},
  booktitle = "Workshop on Deductions Systems for Mathematics Eduation",
  pages = "20-25",
  year = "2000"
  paper = "Farm00.pdf",
  keywords = "axiomref, printed"
}

\end{chunk}

\index{Farmer, William M.}
\begin{chunk}{axiom.bib}
@article{Farm04,
  author = "Farmer, William M.",
  title = {{MKM A New Interdisciplinary Field of Research}},
  journal = "SIGSAM",
  volume = "38",
  pages = "47-52",
  year = "2004",
  abstract =
    "Mathematical Knowledge Management (MKM) is a new interdisciplinary
    field of research in the intersection of mathematics, computer
    science, library science, and scientific publishing. Its objective is
    to develop new and better ways of managing mathematical knowledge
    using sophisticated software tools. Its grand challenge is to create
    a universal digital mathematics library (UDML), accessible via the
    World-Wide Web, that contains essentially all mathematical knowledge
    (intended for the public). The challenges facing MKM are daunting,
    but a UDML, even just partially constructed, would transform how
    mathematics is learned and practiced.",
  paper = "Farm04.pdf",
  keywords = "printed, axiomref"
}

\end{chunk}

\index{Farmer, William M.}
\index{Mohrenschildt, Martin v.}
\begin{chunk}{axiom.bib}
@inproceedings{Farm00a,
  author = "Farmer, William M. and Mohrenschildt, Martin v.",
  title = {{Transformers for Symbolic Computation and Formal Deduction}},
  booktitle = "CADE-17",
  pages = "36-45",
  year = "2000",
  abstract =
    "A transformer is a function that maps expressions to expressions.
    Many transformational operators -— such as expression evaluators and
    simplifiers, rewrite rules, rules of inference, and decision
    procedures -— can be represented by transformers. Computations and
    deductions can be formed by applying sound transformers in
    sequence. This paper introduces machinery for defining sound
    transformers in the context of an axiomatic theory in a formal
    logic. The paper is intended to be a first step in a development of an
    integrated framework for symbolic computation and formal deduction.",
  paper = "Farm00a.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Farmer, William M.}
\index{Larjani, Pouya}
\begin{chunk}{axiom.bib}
@misc{Farm14,
  author = "Farmer, William M. and Larjani, Pouya",
  title = {{Frameworks for Reasoning about Syntax that Utilize
            Quotation and Evaluation}},
  links = "\url{http://imps.mcmaster.ca/doc/syntax.pdf}",
  year = "2014",
  abstract =
    "It is often useful, if not necessary, to reason about the syntactic
    structure of an expression in an interpreted language (i.e., a
    language with a semantics). This paper introduces a mathematical
    structure called a syntax framework that is intended to be an abstract
    model of a system for reasoning about the syntax of an interpreted
    language. Like many concrete systems for reasoning about syntax, a
    syntax framework contains a mapping of expressions in the
    interpreted language to syntactic values that represent the syntactic
    structures of the expressions; a language for reasoning about the
    syntactic values; a mechanism called quotation to refer to the
    syntactic value of an expression; and a mechanism called evaluation to
    refer to the value of the expression represented by a syntactic value.
    A syntax framework provides a basis for integrating reasoning about
    the syntax of the expressions with reasoning about what the
    expressions mean. The notion of a syntax framework is used to discuss
    how quotation and evaluation can be built into a language and to
    define what quasiquotation is. Several examples of syntax frameworks
    are presented.",
  paper = "Farm14.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Carette, Jacques}
\index{Farmer, William M.}
\index{O'Connor, Russell}
\begin{chunk}{axiom.bib}
@misc{Care11c,
  author = "Carette, Jacques and Farmer, William M. and O'Connor, Russell",
  title = {{MathScheme: Project Description}},
  year = "2011",
  link = "\url{http://imps.mcmaster.ca/doc/cicm-2011-proj-desc.pdf}",
  paper = "Care11c.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Carette, Jacques}
\index{Farmer, William M.}
\begin{chunk}{axiom.bib}
@article{Care08,
  author = "Carette, Jacques and Farmer, William M.",
  title = {{High-Level Theories}},
  journal = "LNCS",
  volume = "5144",
  pages = "232-245"
  year = "2008",
  abstract =
    "We introduce high-level theories in analogy with high-level
    programming languages. The basic point is that even though one can
    define many theories via simple, low-level axiomatizations , that is
    neither an effective nor a comfortable way to work with such theories.
    We present an approach which is closer to what users of mathematics
    employ, while still being based on formal structures.",
  paper = "Care08.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Carette, Jacques}
\index{O'Connor, Russell}
\begin{chunk}{axiom.bib}
@article{Care12,
  author = "Carette, Jacques and O'Connor, Russell",
  title = {{Theory Presentation Combinators}},
  journal = "LNCS",
  volume = "7362",
  year = "2012",
  abstract =
    "We motivate and give semantics to theory presentation combinators
    as the foundational building blocks for a scalable library of
    theories. The key observation is that the category of contexts and
    fibered categories are the ideal theoretical tools for this
    purpose.",
  paper = "Care12.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Musser, David R.}
\index{Kapur, Deepak}
\begin{chunk}{axiom.bib}
@article{Muss82,
  author = "Musser, David R. and Kapur, Deepak",
  title = {{Rewrite Rule Theory and Abstract Data Type Analysis}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "77-90",
  year = "1982",
  paper = "Muss82.pdf",
  keywords = "axiomref"
}

\end{chunk}

\index{Lazard, Daniel}
\begin{chunk}{axiom.bib}
@article{Laza82,,
  author = "Lazard, Daniel",
  title = {{Commutative Algebra and Computer Algebra}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "40-48",
  year = "1982",
  abstract =
    "It is well known that computer algebra deals with commutative rings
    such as the integers, the rationals, the modular integers and
    polynomials over such rings.

    On the other hand, commutative algebra is that part of mathematics
    which studies commutative rings.

    Our aim is to make this link more precise. It will appear that most of
    the constructions which appear in classical commutative algebra can be
    done explicitly in finite time. However, there are
    exceptions. Moreover, most of the known algorithms are intractable :
    The problems are generally exponential by themselves, but many
    algorithms are over-over-exponential. It needs a lot of work to find
    better methods, and to implement them, with the final hope to open a
    computation domain larger than this one which is possible by hand.

    To illustrate the limits and the possibilities of computerizing
    commutative algebra, we describe an algorithm which tests the
    primality of a polynomial ideal and we give an example of a single
    algebraic extension of fields $K\subset L$ wuch that there exists an
    algorithm of factorization for the polynomials over $k$, but not for
    the polynomials over $L$.",
  paper = "Laza82.pdf"
}

\end{chunk}

\index{Hearn, Anthony C.}
\begin{chunk}{axiom.bib}
@article{Hear82,,
  author = "Hearn, Anthony C.",
  title = {{REDUCE - A Case Study in Algebra System Development}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "263-272",
  year = "1982",
  paper = "Hear82.pdf",
  keywords = "axiomref"
}

\end{chunk}

\index{Padget, J.A.}
\begin{chunk}{axiom.bib}
@article{Padg82,
  author = "Padget, J.A.",
  title = {{Escaping from Intermediate Expression Swell: A Continuing Saga}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "256-262",
  year = "1982",
  abstract =
    "The notion of a closed continuation is introduced, is presented,
    coroutines using function call and return based on this concept, are
    applications and a functional dialect of LISP shown to be merely a
    more general form of for coroutines in algebraic simplification and
    are suggested, by extension function. expression Potential evaluation
    and a specific example of their use is given in a novel attack on the
    phenomenon of intermediate expression swell in polynomial
    multiplication.",
  paper = "Padg82.pdf"
}

\end{chunk}

\index{Norman, Arthur}
\begin{chunk}{axiom.bib}
@article{Norm82,
  author = "Norman, Arthur",
  title = {{The Development of a Vector-Based Algebra System}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "237-248",
  year = "1982",
  paper = "Norm82.pdf"
}

\end{chunk}

\index{Bordoni, L.}
\index{Colagrossi, A.}
\index{Miola, A.}
\begin{chunk}{axiom.bib}
@article{Bord82,
  author = "Bordoni, L. and Colagrossi, A. and Miola, A.",
  title = {{Linear Algebraic Approach for Computing Polynomial Resultant}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "231-236",
  year = "1982",
  abstract =
    "This paper presents a linear algebraic method for computing the
    resultant of two polynomials. This method is based on the
    computation of a determinant of order equal to the minimum of the
    degrees of the two given polynomials. This method turns out to be
    preferable to other known linear algebraic methods both from a
    computational point of view and for a total generality respect to
    the class of the given polynomials. Some relationships of this
    method with the polynomial pseudo-remainder operation are discussed.",
  paper = "Bord82.pdf"
}

\end{chunk}

\index{Arnon, Dennis S.}
\index{McCallum, Scott}
\begin{chunk}{axiom.bib}
@article{Arno82a,
  author = "Arnon, Dennis S. and McCallum, Scott",
  title = {{Cylindrical Algebraic Decomposition by Quantifier Eliminations}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "215-222",
  year = "1982",
  abstract =
    "Cylindrical algebraic decompositions were introduced as a major
    component of a new quantifier elimination algorithm for elementary
    algebra and geometry (G. Collins, ~973). In the present paper we turn
    the tables and show that one can use quantifier elimination for ele-
    mentary algebra and geometry to obtain a new version of the
    cylindrical algebraic decomposi- tion algorithm. A key part of our
    result is a theorem, of interest in its own right, that relates the
    multiplicities of the roots of a polynomial to their continuity.",
  paper = "Arno82a.pdf"
}

\end{chunk}

\index{Collins, George E.}
\begin{chunk}{axiom.bib}
@article{Coll82a,
  author = "Collins, George E.",
  title = {{Factorization in Cylindrical Algebraic Decomposition - Abstract}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "212-214",
  year = "1982",
  paper = "Coll82a.pdf"
}

\end{chunk}

\index{Lazard, Daniel}
\begin{chunk}{axiom.bib}
@article{Laza82a,
  author = "Lazard, Daniel",
  title = {{On Polynomial Factorization}},
  journal = "Lecture Notes in Computer Science",
  volume = "144",
  pages = "144-157",
  year = "1982",
  abstract =
    "We present new algorithms for factoring univariate polynomials
    over finite fields. They are variants of the algorithms of Camion
    and Cantor-Zassenhaus and differ from them essentially by
    computing the primitive idempotents of the algebra $K[X]/f$ before
    factoring $f$.

    These algorithms are probabilistic in the following sense. The
    time of computation depends on random choices, but the validity of
    the result does not depend on them. So, worst case complexity,
    being infinite, is meaningless and we compute average
    complexity. It appears that our and Cantor-Zassenhaus algorithms
    have the same asymptotic complexity and they are the best
    algorithms actuall known; with elementary multiplication and GCD
    computation, Cantor-Zassenhaus algorithm is always bettern than
    ours; with fast multiplication and GCD, it seems that ours is
    better, but this fact is not yet proven.

    Finally, for factoring polynomials over the integers, it seems
    that the best strategy consists in choosing prime moduli as big as
    possible in the range where the time of the multiplication does
    not depend on the size of the factors (machine word size). An
    accurate computation of the involved constants would be needed for
    proving this estimation.",
  paper = "Laza82a.pdf"
}

\end{chunk}

\index{Strachey, Christopher}
\index{Wadsworth, Christopher}
\begin{chunk}{axiom.bib}
@article{Stra00a,
  author = "Strachey, Christopher and Wadsworth, Christopher",
  title = {{Continuations: A Mathematical Semantics for Handling Full Jumps}},
  journal = "Higher-Order and Symbolic Computation",
  volume = "13",
  pages = "135-152",
  year = "2000",
  abstract =
    "This paper describes a method of giving the mathematical
    semantics of programming languages which include the most general
    form of jumps.",
  paper = "Stra00a.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Kaes, Stefan}
\begin{chunk}{axiom.bib}
@article{Kaes88,
  author = "Kaes, Stefan",
  title = {{Parametric Overloading in Polymorphic Programming Languages}},
  journal = "LNCS",
  volume = "300",
  pages = "131-144",
  year = "1988",
  abstract =
    "The introduction of unrestricted overloading in languagues with type
    systems based on implicit parametric potymorphism generally destroys
    the principal type property: namely that the type of every expression
    can uniformly be represented by a single type expression over some set
    of type variables. As a consequence, type inference in the presence
    of unrestricted overloading can become a NP-complete problem. In
    this paper we define the concept of parametric overloading as a
    restricted form of overloading which is easily combined with
    parametric polymorphism. Parametric overloading preserves the
    principal type property, thereby allowing the design of efficient type
    inference algorithms. We present sound type deduction systems, both
    for predefined and programmer defined overloading. Finally we state
    that parametric overloading can be resolved either statically, at
    compile time, or dynamically, during program execution.",
  paper = "Kaes88.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Kaes, Stefan}
\begin{chunk}{axiom.bib}
@article{Kaes92,
  author = "Kaes, Stefan",
  title = {{Type Inference inthe Presence of Overloading, Subtyping and
            Recursive Types}},
  journal = "ACM Lisp Pointers",
  volume = "5",
  number = "1",
  year = "1992",
  pages = "193-204",
  abstract =
    "We present a unified approach to type inference in the presence of
    overloading and coercions based on the concept of {\sl constrained
    types}. We define a generic inference system, show that subtyping and
    overloading can be treated as a special instance of this system and
    develop a simple algorithm to compute principal types. We prove the
    decidability of type inference for hte class of {\sl decomposable
    predicates} and deelop a canonical representation for principal types
    based on {\sl most accurate simplifications} of constraint
    sets. Finally, we investigate the extension of our techniques to
    {\sl recursive types}.",
  paper = "Kaes92.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Hall, Cordelia V.}
\index{Hammond, Kevin}
\index{Jones, Simon L. Peyton}
\index{Wadler, Philip L.}
\begin{chunk}{axiom.bib}
@article{Hall96,
  author = "Hall, Cordelia V. and Hammond, Kevin and Jones, Simon L. Peyton
            and Wadler, Philip L.",
  title = {{Type Classes in Haskell}},
  journal = "Trans. on Programming Langues and Systems",
  volume = "18",
  number = "2",
  pages = "109-138",
  year = "1996",
  abstract =
    "This article de nes a set of type inference rules for resolving
    overloading introduced by type classes, as used in the functional
    programming language Haskell. Programs including type classes are
    transformed into ones which may be typed by standard Hindley-Milner
    inference rules. In contrast to other work on type classes, the rules
    presented here relate directly to Haskell programs. An innovative
    aspect of this work is the use of second-order lambda calculus to
    record type information in the transformed program.",
  paper = "Hall96.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Dreyer, Derek}
\index{Harper, Robert}
\index{Chakravarty, Manuel M.T.}
\index{Keller, Gabriele}
\begin{chunk}{axiom.bib}
@inproceedings{Drey07,
  author = "Dreyer, Derek and Harper, Robert and Chakravarty, Manuel M.T.
            and Keller, Gabriele",
  title = {{Modlular Type Classes}},
  booktitle = "Proc. POPL'07",
  pages = "63-70",
  year = "2007",
  abstract =
    "ML modules and Haskell type classes have proven to be highly
    effective tools for program structuring. Modules emphasize explicit
    configuration of program components and the use of data abstraction.
    Type classes emphasize implicit program construction and ad hoc
    polymorphism. In this paper , we show how the implicitly-typed
    style of type class programming may be supported within the framework
    of an explicitly-typed module language by viewing type classes as a
    particular mode of use of modules. This view offers a harmonious
    integration of modules and type classes, where type class features,
    such as class hierarchies and associated types, arise naturally as
    uses of existing module-language constructs, such as module
    hierarchies and type components. In addition, programmers have
    explicit control over which type class instances are available for
    use by type inference in a given scope. We formalize our approach as
    a Harper-Stone-style elaboration relation, and provide a sound type
    inference algorithm as a guide to implementation.",
  paper = "Drey07.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Wehr, Stefan}
\index{Chakravarty, Maneul M.T.}
\begin{chunk}{axiom.bib}
@article{Wehr08,
  author = "Wehr, Stefan and Chakravarty, Maneul M.T.",
  title = {{ML Modules and Haskell Type Classes: A Constructive
            Comparison}},
  journal = "LNCS",
  volume = "5356",
  pages = "188-204",
  year = "2008",
  abstract =
    "Researchers repeatedly observed that the module system of ML and the
    type class mechanism of Haskell are related. So far, this relationship
    has received little formal investigation. The work at hand fills this
    gap: It introduces type-preserving translations from modules to type
    classes and vice versa, which enable a thorough comparison of the two
    concepts.",
  paper = "Wehr08.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Stuckey, Peter J.}
\index{Sulzmann, Martin}
\begin{chunk}{axiom.bib}
@article{Stuc05,
  author = "Stuckey, Peter J. and Sulzmann, Martin",
  title = {{A Theory of Overloading}},
  journal = "ACM Trans. on Programming Languages and Systems",
  volume = "27",
  number = "6",
  pages = "1-54",
  year = "2005",
  abstract =
    "We present a novel approach to allow for overloading of
    identifiers in the spirit of type classes. Our approach relies on
    the combination of the HM(X) type system framework with Constraint
    Handling Rules (CHRs). CHRs are a declarative language for writing
    incremental constraint solvers, that provide our scheme with a
    form of programmable type language. CHRs allow us to precisely
    describe the relationships among overloaded identifiers. Under
    some sufficient conditions on the CHRs we achieve decidable type
    inference and the semantic meaning of programs is unambiguous. Our
    approach provides a common formal basis for many type class
    extensions such as multi-parameter type classes and functional
    dependencies.",
  paper = "Stuc05.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Reynolds, J.C.}
\begin{chunk}{axiom.bib}
@article{Reyn85,
  author = "Reynolds, J.C.",
  title = {{Three Approaches to Type Structure}},
  journal = "LNCS",
  volume = "185",
  year = "1985",
  abstract =
    "We examine three disparate views of the type structure of
    programming languages: Milner's type deduction system and polymorphic
    let construct, the theory of subtypes and generic operators, and
    the polymorphic or second-order typed lambda calculus. These
    approaches are illustrated with a functional language including
    product, sum and list constructors. The syntactic behavior of types
    is formalized with type inference rules, bus their semantics is
    treated intuitively.",
  paper = "Reyn85.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Balsters, Herman}
\index{Fokkinga, Maarten M.}
\begin{chunk}{axiom.bib}
@article{Bals91,
  author = "Balsters, Herman and Fokkinga, Maarten M.",
  title = {{Subtyping can have a simple semantics}},
  journal = "Theoretical Computer Science",
  volume = "87",
  pages = "81-96",
  year = "1991",
  abstract =
    "Consider a first order typed language, with semantics
     $\llbracket~\rrbracket$ for expressions and types. Adding
     subtyping means that a partial order $\le$ on types is defined
     and that the typing rules are extended to the effect that
     expression $e$ has type $\tau$ whenever $e$ has type $\sigma$ and
     $\sigma \le \tau$. We show how to adapt the semantics
     $\llbracket~\rrbracket$ in a {\sl simple set theoretic way},
     obtaining a semantics $\llbracket~\rrbracket$ that satisfies, in
     addition to some obvious requirements, also the property
     $\llbracket\sigma\rrbracket \subseteq $\llbracket\tau\rrbracket$,
     whenever $\sigma \le \tau$.",
  paper = "Bals91.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Cardelli, Luca}
\begin{chunk}{axiom.bib}
@article{Card84,
  author = "Cardelli, Luca",
  title = {{A Semantics of Multiple Inheritance}},
  journal = "LNCS",
  volume = "173",
  year = "1984",
  paper = "Card84.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Mosses, Peter}
\begin{chunk}{axiom.bib}
@article{Moss84,
  author = "Mosses, Peter",
  title = {{A Basic Abstract Semantics Algebra}},
  journal = "LNCS",
  volume = "173",
  year = "1984",
  abstract =
    "It seems that there are some pragmatic advantages in using Abstract
    Semantic Algebras (ASAs) instead of X-notation in denotational
    semantics. The values of ASAs correspond to 'actions' (or
    'processes'), and the operators correspond to primitive ways of
    combining actions. There are simple ASAs for the various independent
    'facets' of actions: a functional ASA for data-flow, an imperative ASA
    for assignments, a declarative ASA for bindings, etc. The aim is to
    obtain general ASAs by systematic combination of these simple ASAs.

    Here we specify a basic ASA that captures the common features of the
    functional, imperative and declarative ASAs -- and highlights their
    differences. We discuss the correctness of ASA specifications, and
    sketch the proof of the consistency and (limiting) completeness of the
    functional ASA, relative to a simple model.

    Some familiarity with denotational semantics and algebraic
    specifications is assumed.",
  paper = "Moss84.pdf"
}

\end{chunk}

\index{Gross, Jason}
\index{Chlipala, Adam}
\begin{chunk}{axiom.bib}
@misc{Gros15,
  author = "Gross, Jason and Chlipala, Adam",
  title = {{Parsing Parses}},
  link = "\url{https://people.csail.mit.edu/jgross/personal-website/papers/2015-parsing-parse-trees.pdf}",
  year = "2015",
  abstract =
    "We present a functional parser for arbitrary context-free grammars,
    together with soundness and completeness proofs, all inside Coq. By
    exposing the parser in the right way with parametric polymorphism and
    dependent types, we are able to use the parser to prove its own
    soundness, and, with a little help from relational parametricity,
    prove its own completeness, too. Of particular interest is one strange
    instantiation of the type and value parameters: by parsing parse trees
    instead of strings, we convince the parser to generate its own
    completeness proof. We conclude with highlights of our experiences
    iterating through several versions of the Coq development, and some
    general lessons about dependently typed programming.",
  paper = "Gros15.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Wehr, Stefan}
\begin{chunk}{axiom.bib}
@phdthesis{Wehr05,
  author = "Wehr, Stefan",
  title = {{ML Modules and Haskell Type Classes: A Constructive
            Comparison}},
  school = "Albert Ludwigs Universitat",
  year = "2005",
  abstract =
    "Researchers repeatedly observed that the module system of ML and the
    type class mechanism of Haskell are related. So far, this relationship
    has received little formal investigation. The work at hand fills this
    gap: It introduces type-preserving translations from modules to type
    classes and vice versa, which enable a thorough comparison of the two
    concepts.

    The source language of the first translation is a subset of
    Standard ML. The target language is Haskell with common extensions
    and one new feature, which was deeloped as part of this work. The
    second translation maps a subset of Haskell 98 to ML, with
    well-established extensions. I prove that the translations
    preserve type correctness and provide implementations for both.

    Building on the insights obtained from the translations, I present
    a thorough comparison between ML modules and Haskell type
    classes. Moreover, I evaluate to what extent the techniques used
    in the translations can be exploited for modular programming in
    Haskell and for programming with ad-hoc polymorphism in ML.",
  paper = "Wehr05.pdf"
}

\end{chunk}

\index{Dreyer, Derek}
\index{Crary, Karl}
\index{Harper, Robert}
\begin{chunk}{axiom.bib}
@article{Drey03,
  author = "Dreyer, Derek and Crary, Karl and Harper, Robert",
  title = {{A Type System for Higher-Order Modules}},
  journal = "ACM SIGPLAN Notices",
  volume = "38",
  number = "1",
  year = "2003",
  link = "\url{https://www.cs.cmu.edu/~crary/papers/2003/thoms/thoms.pdf}",
  abstract =
    "We present a type theory for higher-order modules that accounts for
    many central issues in module system design, including translucency,
    applicativity , generativity , and modules as first-class values.
    Our type system harmonizes design elements from previous work,
    resulting in a simple, economical account of modular programming. The
    main unifying principle is the treatment of abstraction mechanisms
    as computational effects. Our language is the first to provide a
    complete and practical formalization of all of these critical issues
    in module system design.",
  paper = "Drey03.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Crary, Karl}
\index{Harper, Robert}
\index{Puri, Sidd}
\begin{chunk}{axiom.bib}
@inproceedings{Crar99,
  author = "Crary, Karl and Harper, Robert and Puri, Sidd",
  title = {{What is a Recursive Module}},
  booktitle = "Conf. on Programming Language Design and Implementation",
  year = "1999",
  link = "\url{https://www.cs.cmu.edu/~crary/papers/1999/recmod/recmod.dvi}",
  abstract =
    "A hierarchical module system is an effective tool for structuring
    large programs. Strictly hierarchical module systems impose an
    acyclic ordering on import dependencies among program units. This
    can impede modular programming by forcing mutually-dependent
    components to be consolidated into a single module. Recently there
    have been several proposals for module systems that admit cyclic
    dependencies, but it is not clear how these proposals relate to
    one another, nor how one mught integrate them into an expressive
    module system such as that of ML.

    To address this question we provide a type-theoretic analysis of
    the notion of a recursive module in the context of a
    ``phase-distinction'' formalism for higher-order module
    systems. We extend this calculus with a recursive module mechanism
    and a new form of signature, called a {\sl recurslively dependent
    signature}, to support the definition of recursive modules. These
    extensions are justified by an interpretation in terms of more
    primitive language constructs. This interpretation may also serve
    as a guide for implementation.",
  paper = "Crar99.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Dreyer, Derek}
\index{Crary, Karl}
\index{Harper, Robert}
\begin{chunk}{axiom.bib}
@techreport{Drey02,
  author = "Dreyer, Derek and Crary, Karl and Harper, Robert",
  title = {{A Type System for Higher-Order Modules (Expanded Version)}},
  type = "technical report",
  institution = "Carnegie Mellon University",
  number = "CMU-CS-02-122R",
  year = "2002",
  link = "\url{https://www.cs.cmu.edu/~crary/papers/2003/thoms/thoms-tr.pdf}",
  abstract =
    "We present a type theory for higher-order modules that accounts for
    many central issues in module system design, including translucency,
    applicativity , generativity , and modules as first-class values.
    Our type system harmonizes design elements from previous work,
    resulting in a simple, economical account of modular programming. The
    main unifying principle is the treatment of abstraction mechanisms
    as computational effects. Our language is the first to provide a
    complete and practical formalization of all of these critical issues
    in module system design.",
  paper = "Drey02.pdf"
}

\end{chunk}

\index{Crary, Karl}
\begin{chunk}{axiom.bib}
@techreport{Crar02,
  author = "Crary, Karl",
  title = {{Toward a Foundational Typed Assembly Language}},
  institution = "Carnegie Mellon University",
  number = "CMU-CS-02-196",
  year = "2002,
  link = "\url{https://www.cs.cmu.edu/~crary/papers/2003/talt/talt-tr.pdf}",
  abstract =
    "We present the design of a typed assembly language called TALT that
    supports heterogeneous tuples, disjoint sums, arrays, and a general
    account of addressing modes. TALT also implements the von Neumann
    model in which programs are stored in memory, and supports relative
    addressing. Type safety for execution and for garbage collection are
    shown by machine-checkable proofs. TALT is the first formalized typed
    assembly language to provide any of these features.",
  paper = "Crar02.pdf"
}

\end{chunk}

\index{Mili, Ali}
\index{Aharon, Shir}
\index{Nadkarni, Chaitanya}
\begin{chunk}{axiom.bib}
@article{Mili09,
  author = "Mili, Ali and Aharon, Shir and Nadkarni, Chaitanya",
  title = {{Mathematics for Reasoning about Loop Functions}},
  journal = "Science of Computer Programming",
  volume = "79",
  year = "2009",
  pages = "989-1020",
  abstract =
    "The criticality of modern software applications, the pervasiveness of
    malicious code concerns, the emergence of third-party software
    development, and the preponderance of program inspection as a quality
    assurance method all place a great premium on the ability to analyze
    programs and derive their function in all circumstances of use and all
    its functional detail. For C-like programming languages, one of the
    most challenging tasks in this endeavor is the derivation of loop
    functions. In this paper, we outline the premises of our approach to
    this problem, present some mathematical results, and discuss how these
    results can be used as a basis for building an automated tool that
    derives the function of while loops under some conditions.",
  paper = "Mili09.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Piroi, Florina}
\index{Buchberger, Bruno}
\index{Rosenkranz, Camelia}
\begin{chunk}{axiom.bib}
@misc{Piro08,
  author = "Piroi, Florina and Buchberger, Bruno and Rosenkranz, Camelia",
  title = {{Mathematical Journals as Reasoning Agents: Literature Review}},
  year = "2008",
  link = "\urlhttp://www.risc.jku.at/publications/download/risc_3442/Math-Agents-for-SFB-2008-03-10-12h00.pdf{}",
  abstract =
    "This report reviews the literature relevant for the research project
    'Math−Agents: Mathematical Journals as Reasoning Agents' proposed by
    Bruno Buchberger as a technology transfer project based on the results
    of the SFB Project 'Scientific Computing', in particular the project
    SFB 1302, 'Theorema'. The project aims at computer−supporting the
    refereeing process of mathematical journals by tools that are mainly
    based on automated reasoning and also at building up the knowledge
    archived in mathematical journals in such a way that they can act as
    interactive and active reasoning agents later on. In this report,
    we review current mathematical software systems with a focus on the
    availability of tools that can contribute to the goals of the Math−
    Agents project.",
  paper = "Piro08.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Sokolowski, Stefan}
\begin{chunk}{axiom.bib}
@article{Soko87,
  author = "Sokolowski, Stefan",
  title = {{Soundness of Hoare's Logic: An Automated Proof Using LCF}},
  journal = "Trans. on Programming Languages and Systems",
  volume = "9",
  number = "1",
  pages = "100-120",
  year = "1987",
  abstract =
    "This paper presents a natural deduction proof of Hoare's logic
    carried out by the Edinburgh LCF theorem prover. The emphasis is
    on the way Hoare's theory is presented to the LCF, which looks
    very much like an exposition of syntax and semantics to human
    readers; and on the programmable heuristics (tactics). We also
    discuss some problems and possible improvements to the LCF.",
  paper = "Soko87.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Wadler, Philip}
\begin{chunk}{axiom.bib}
@article{Wadl95,
  author = "Wadler, Philip",
  title = {{Monads for Functional Programming}},
  journal = "LNCS",
  volume = "925",
  abstract =
    "The use of monads to structure functional programs is
    described. Monads provide a convenient framework for simulating
    effects found in other languages, such as global state, exception
    handling, output, or non-determinism. Three case studies are
    looked at in detail: how monads ease the modification of a simple
    evaluator; how monads act as the basis of a datatype of arrays
    subject to in-place update; and how monads can be used to build
    parsers.",
  paper = "Wadl95.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Freeman, Tim}
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@inproceedings{Free91,
  author = "Freeman, Tim and Pfenning, Frank",
  title = {{Refinement Types for ML}},
  booktitle = "ACM SIGPLAN PLDI'91",
  year = "1991",
  link = "\url{http://www.cs.cmu.edu/~fp/papers/pldi91.pdf}",
  abstract =
    "We describe a refinement of ML's type system allowing the
    specification of recursively defined subtypes of user-defined
    datatypes. The resulting system of {\sl refinement types}
    preserves desirable properties of ML such as decidability of type
    inference, while at the same time allowing more errors to be
    detected at compile-time. The type system combines abstract
    interpretation with ideas from the intersection type discipline,
    but remains closely tied to ML in that refinement types are given
    only to programs which are already well-typed in ML.",
  paper = "Free91.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Zeilberger, Noam}
\begin{chunk}{axiom.bib}
@misc{Zeil16,
  author = "Zeilberger, Noam",
  title = {{Towards a Mathematical Science of Programming}},
  year = "2016"
}

\end{chunk}

\index{Zeilberger, Noam}
\begin{chunk}{axiom.bib}
@inproceedings{Zeil16a,
  author = "Zeilberger, Noam",
  title = {{Principles of Type Refinement}},
  booktitle = "OPLSS 2106",
  link = "\url{http://noamz.org/oplss16/refinements-notes.pdf}",
  year = "2016",
  paper = "Zeil16a.pdf"
}

\end{chunk}

\index{McCarthy, John}
\begin{chunk}{axiom.bib}
@incollection{Mcca63,
  author = "McCarthy, John",
  title = {{A Basis for a Mathematical Theory of Computation}},
  booktitle = "Computer Programming and Formal Systems",
  year = "1963",
  paper = "Mcca63.pdf"
}

\end{chunk}

\index{Scott, Dana S.}
\index{Strachey, Christopher}
\begin{chunk}{axiom.bib}
@article{Scot71,
  author = "Scott, Dana S. and Strachey, C.",
  title = {{Towards a Mathematical Semantics for Computer Languages}},
  journal = "Proc. Symp. on Computers and Automata",
  volume = "21",
  year = "1971",
  abstract =
    "Compilers for high-level languages are generally constructed to
    give a complete translation of the programs into machine
    lanugage. As machines merely juggle bit patterns, the concepts of
    the original language may be lost or at least obscured during this
    passage. The purpose of a mathematical semantics is to give a
    correct and meaningful correspondence between programs and
    mathematical entities in a way that is entirely independent of an
    implementation. This plan is illustrated in a very elementary
    method with the usual idea of state transformations. The next
    section shows why the mathematics of functions has to be modified
    to accommodate recursive commands. Section 3 explains the
    modification. Section 4 introduces the environments for handling
    variables and identifiers and shows how the semantical equations
    define equivalence of programs. Section 5 gives an exposition of
    the new type of mathematical function spaces that are required for
    the semantics of procedures when these are allowed in assignment
    statements. The conclusion traces some of the background of the
    project and points the way to future work.",
  paper = "Scot71.pdf"
}

\end{chunk}

\index{Mellies, Paul-Andre}
\index{Zeilberger, Noam}
\begin{chunk}{axiom.bib}
@inproceedings{Mell15,
  author = "Mellies, Paul-Andre and Zeilberger, Noam",
  title = {{Functors are Type Refinement Systems}},
  booktitle = "POPL'15",
  publisher = "ACM",
  year = "2015",
  abstract =
    "The standard reading of type theory through the lens of category
    theory is based on the idea of viewing a type system as a category
    of well-typed terms. We propose a basic revision of this reading;
    rather than interpreting type systems as categories, we describe
    them as {\sl functors} from a category of typing derivations to a
    category of underlying terms. Then, turning this around, we
    explain how in fact {\sl any} functor gives rise to a generalized
    type system, with an abstract notion of type judgment, typing
    derivations and typing rules. This leads to a purely categorical
    reformulation of various natural classes of type systems as
    natural classes of functors.

    The main purpose of this paper is to describe the general
    framework (which can also be seen as providing a categorical
    analysis of {\sl refinement types}, and to present a few
    applications. As a larger case study, we revisit Reynold's paper
    on ``The Meaning of Types'' (2000), showing how the paper's main
    results may be reconstructed along these lines.",
  paper = "Mell15.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Shields, Mark}
\index{Jones, Simon Peyton}
\begin{chunk}{axiom.bib}
@inproceedings{Shie02,
  author = "Shields, Mark and Jones, Simon Peyton",
  title = {{First-Class Modules for Haskell}},
  booktitle = "9th Int. Conf. on Foundations of Object-Oriented Languages",
  pages = "28-40",
  year = "2002",
  link = "\url{http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/first_class_modules.pdf}",
  abstract =
    "Though Haskell's module language is quite weak, its core language
    is highly expressive. Indeed, it is tantalisingly close to being
    able to express much of the structure traditionally delegated to a
    separate module language. However, the encoding are awkward, and
    some situations can't be encoded at all.

    In this paper we refine Haskell's core language to support
    {\sl first-class modules} with many of the features of ML-style
    modules. Our proposal cleanly encodes signatures, structures and
    functors with the appropriate type abstraction and type sharing,
    and supports recursive modules. All of these features work across
    compilation units, and interact harmoniously with Haskell's class
    system. Coupled with support for staged computation, we believe
    our proposal would be an elegant approach to run-time dynamic
    linking of structured code.

    Our work builds directly upon Jones' work on parameterised
    signatures, Odersky and L\"aufer's system of higher-ranked type
    annotations, Russo's semantics of ML modules using ordinary
    existential and universal quantifications, and Odersky and
    Zenger's work on nested types. We motivate the system by examples,
    and include a more formal presentation in the appendix.",
  paper = "Shie02.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Dijkstra, E.W.}
\begin{chunk}{axiom.bib}
@misc{Dijk71,
  author = "Dijkstra, E.W.",
  title = {{A Short Introduction to the Art of Programming}},
  comment = "EWD316",
  year = "1971",
  paper = "Dijk71.pdf"
}

\end{chunk}

\index{Steele, Guy Lewis}
\index{Sussman, Gerald Jay}
\begin{chunk}{axiom.bib}
@techreport{Stee78a,
  author = "Steele, Guy Lewis and Sussman, Gerald Jay",
  title = {{The Art of the Interpreter or, The Modularity Complex (Parts
            Zero, One, and Two}},
  type = "technical report",
  institution = "MIT AI Lab",
  number = "AIM-453",
  year = "1978",
  abstract =
    "We examine the effects of various language design decisions on
    the programming styles available to a user of the language, with
    particular emphasis on the ability to incrementally construct
    modular systems. At each step we exhibit an interactive
    meta-circular interpreter for the language under consideration.

    We explore the consequences of various variable binding
    disciplines and the introduction of side effects. We find that
    dynamic scoping is unsuitable for constructing procedural
    abstractions, but has another role as an agent of modularity,
    being a structured form of side effect. More general side effects
    are also found to be necessary to promote modular style. We find
    that the notion of side effect and the notion of equality (object
    identity) are mutually constraining: to define one is to define
    the other.

    The interpreters we exhibit are all written in a simple dialect of
    LISP, and all implement LISP-like languages. A subset of these
    interpreters constitute a partial historical reconstruction of the
    actual evolution of LISP.",
  paper = "Stee78a.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Wadler, Philip}
\index{Findler, Robert Bruce}
\begin{chunk}{axiom.bib}
@inproceedings{Wadl07a,
  author = "Wadler, Philip and Findler, Robert Bruce",
  title = {{Well-Typed Programs Can't Be Blamed}},
  booktitle = "Workshop on Scheme and Functional Programming",
  year = "2007",,
  pages = "15-26",
  abstract =
    "We show how {\sl contracts} with blame fit naturally with recent
    work on {\sl hybrid types} and {\sl gradual types}. Unlike hybrid
    types or gradual types, we require casts in the source code, in
    order to indicate where type errors may occur. Two (perhaps
    surprising) aspects of our approach are that refined types can
    provide useful static guarantees even in the absence of a theorem
    prover, and that type {\sl dynamic} should not be regarded as a
    supertype of all other types. We factor the well-known notion of
    subtyping into new notions of positive and negative subtyping, and
    use these to characterise where positive and negative blame may
    arise. Our approach sharpens and clarifies some recent results in
    the literature.",
  paper = "Wadl07a.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Michaelson, Greg}
\begin{chunk}{axiom.bib}
@book{Mich11,
  author = "Michaelson, Greg",
  title = {{Functional Programming Through Lambda Calculus}},
  year = "2011",
  publisher = "Dover",
  isbn = "978-0-486-47883-8"
}

\end{chunk}

Author: jomae
Revision Date: 2018-05-16 06:37:27 UTC

1.3.3dev: follow-up to r16603, add omitted changes in logging (refs #12993)

Author: Amadeusz Sławiński
Revision Date: 2018-05-15 19:20:27 UTC

this actually should be 3 dots

they are part of syntax

Author: Paolo Bacchilega
Revision Date: 2018-05-15 08:31:08 UTC

image loader: clear the image if the operation was cancelled

Author: SharkCZ
Revision Date: 2018-05-14 20:31:49 UTC

vmx: Fix vector loads on ppc64le

Use vector intrinsic for loading possibly unaligned data instead of a
typecast.

Bugzilla: https://bugzilla.redhat.com/1572540
Signed-off-by: Dan Horák <dan@danny.cz>
Signed-off-by: Adam Jackson <ajax@redhat.com>
Tested-by: Matt Turner <mattst88@gmail.com>
Reviewed-by: Siarhei Siamashka <siarhei.siamashka@gmail.com>

Author: Robert Antoni Buj Gelonch
Revision Date: 2018-05-14 10:31:52 UTC

I18n: Update translation ca (100%).

376 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Robert Antoni Buj Gelonch
Revision Date: 2018-05-14 10:31:36 UTC

I18n: Update translation ca (100%).

178 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Robert Antoni Buj Gelonch
Revision Date: 2018-05-14 10:30:17 UTC

I18n: Update translation ca (100%).

175 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Andreas Schneider
Revision Date: 2018-05-14 06:17:08 UTC

wrapper: Fix memory leak when freeing server_pubkey

Thanks to John McVann.

Signed-off-by: Andreas Schneider <asn@cryptomilk.org>

Author: Sebastian Geiger
Revision Date: 2018-05-13 14:13:58 UTC

tilda.c: simplify logging workarounds

Author: Clement Lefebvre
Revision Date: 2018-05-12 12:23:23 UTC

7.9.2

Author: Chris Wilson
Revision Date: 2018-05-12 09:01:10 UTC

configure: Set DRI1 to autodiscover

We only need DRI1 to support UMS on i810, but modern Xservers don't
support DRI1 and the support infrastructure is no longer being shipped
on some distributions. Gracefully fail if we can't compile the DRI1
code blocks for i810.

Signed-off-by: Chris Wilson <chris@chris-wilson.co.uk>

Author: Peter Bloomfield
Revision Date: 2018-05-11 00:20:40 UTC

Use GResource instead of installed files

Current Balsa uses installed ui/*.ui files to define the user interfaces
for the main window, the message window, the compose window, and the
view-source window. Those files can be replaced by GResource objects,
which are part of the binary file, so that accessing them requires no
additional file system access.

This commit:
• changes the C code to use GResources instead of installed files;
• changes various meson.build files to generate the necessary C files
  instead of installing XML ui files (not difficult);
• changes configure.ac and various Makefile.am files for the same
  purpose (far more difficult, for me!).

Author: Guillem Jover
Revision Date: 2018-05-10 13:08:02 UTC

dpkg-divert: Do not assume that diversions are always present

Several code paths assumed that the fsys nodes were only present when
they contained diversions, and no other nodes would be present, thus
did not make sure to check whether the divert struct members were valid.

With the switch to a single fsys underlying implementation now triggers
can vivify namenodes in the hash, so we need to check whether the members
are valid all the time.

Fixes: commit 2d7566140335d5338e5a98278d4df762936f67f4
Reported-by: Sven Joachim <svenjoac@gmx.de>
Bisected-by: Sven Joachim <svenjoac@gmx.de>

Author: zvacet
Revision Date: 2018-05-09 10:30:46 UTC

I18n: Update translation hr (100%).

77 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Geza Kovacs
Revision Date: 2018-05-09 04:18:19 UTC

fixed unetbootin_asroot script

Author: John Ralls
Revision Date: 2018-05-09 00:55:35 UTC

Restore scaling of CoreText fonts.

Fixes bug 787867.

Author: Bryce Harrington
Revision Date: 2018-05-07 23:50:42 UTC

Drop stray patch from prior commit

Author: Clement Lefebvre
Revision Date: 2018-05-07 11:31:55 UTC

4.1.2

Author: kfujino
Revision Date: 2018-05-07 05:35:01 UTC

Remove unnecessary default property values.

Author: reimar
Revision Date: 2018-05-06 20:08:10 UTC

Use thin .a files if possible.

Instead of copying all .o files, the .a file
just has the symbol index and references to the
.o files in thin mode.
As we never install the .a files anywhere, that
makes more sense for us, reducing disk usage
and I/O requirements when building.

Author: Robert Antoni Buj Gelonch
Revision Date: 2018-05-05 22:31:55 UTC

I18n: Update translation ca (100%).

1030 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Balázs Meskó
Revision Date: 2018-05-05 12:33:15 UTC

Update Hungarian translation

(cherry picked from commit b78528cbb51804be06b29ec65df4333624a2d734)

Author: lbeltrame
Revision Date: 2018-05-05 07:32:08 UTC

Allow building with Qt 5.11

qt5_use_modules is no longer present in Qt 5.11. Fix build by
moving to target_link_libraries
This also adds a dependency on Qt5 Widgets (used by the test)

Author: Bruno Haible
Revision Date: 2018-05-04 19:48:35 UTC

Drop special instructions for OSF/1.

Author: Emin Tufan Çetin
Revision Date: 2018-05-03 07:02:30 UTC

Update Turkish translation

Author: Jean Delvare
Revision Date: 2018-05-03 06:33:24 UTC

quiltrc: Support all patch formats by default

Passing --unified to patch by default prevents using other patch
formats. Out of curiosity, I checked if it helped with performance
but was not able to measure any improvement. So stop passing
--unified by default.

Signed-off-by: Jean Delvare <jdelvare@suse.de>

Author: Erik Ogenvik
Revision Date: 2018-04-30 21:15:12 UTC

Fixed incorrect method call.

Author: Daniel Mustieles
Revision Date: 2018-04-30 14:14:43 UTC

Updated Spanish translation

Author: Andre Miranda
Revision Date: 2018-04-29 16:30:02 UTC

I18n: Update translation sv (100%).

298 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Balázs Meskó
Revision Date: 2018-04-28 22:35:09 UTC

I18n: Update translation hu (100%).

68 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Balázs Meskó
Revision Date: 2018-04-28 22:31:57 UTC

I18n: Update translation hu (100%).

306 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: Emanuele Petriglia
Revision Date: 2018-04-28 10:30:17 UTC

I18n: Update translation it (100%).

7 translated messages.

Transifex (https://www.transifex.com/xfce/public/).

Author: David Faure
Revision Date: 2018-04-26 17:14:48 UTC

Check 128 bytes rather than 32.

https://bugs.freedesktop.org/show_bug.cgi?id=97372

Author: Bruno Haible
Revision Date: 2018-04-24 07:25:10 UTC

Support input files with CR/LF line terminators.

Author: W. Michael Petullo
Revision Date: 2018-04-23 04:42:57 UTC

Fix pedansee warnings in dmap-mdns-avahi.c

Signed-off-by: W. Michael Petullo <mike@flyn.org>

Author: lantw44
Revision Date: 2018-04-22 10:46:31 UTC

build: Change header installation directory back to gtkhex-3

This is what autotools build used to use, and it makes it consistent
with the .pc file.

https://bugzilla.gnome.org/show_bug.cgi?id=789118

Author: Spencer Jackson
Revision Date: 2018-04-17 21:36:00 UTC

adding z plane pole mapping script

Author: Sebastien Bacher
Revision Date: 2018-04-17 14:58:26 UTC

Don't create the user config dir as world readable

https://bugzilla.gnome.org/show_bug.cgi?id=792677

Author: Rūdolfs Mazurs
Revision Date: 2018-04-11 16:12:31 UTC

Update Latvian translation

(cherry picked from commit 7daa48bed9958fdc10f50e40826621281fb9f842)

Author: Matej Urbančič
Revision Date: 2018-04-10 20:19:41 UTC

Updated Slovenian translation

Author: Matej Urbančič
Revision Date: 2018-04-10 20:18:08 UTC

Updated Slovenian translation

Author: Jiri Grönroos
Revision Date: 2018-04-10 17:58:25 UTC

Update Finnish translation