Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ Upstream-Name: lem Upstream-Contact: Lem Devs Source: https://github.com/rems-project/lem Files-Excluded: doc/built-doc/html-doc/*.html doc/built-doc/*.html doc/built-doc/*.pdf doc/lem-draft.pdf ocaml-lib/dependencies manual examples/ppcmem-model Files: * Copyright: 2010-2024 Dominic Mulligan, Kathryn E. Gray, Scott Owens, Peter Sewell, Thomas Tuerk, Basile Clement, Brian Campbell, Christopher Pulte, David Sheets, Fabian Immler Frederic Loulergue, Francesco Zappa Nardelli. Gabriel Kerneis, James Lingard, Jean Pichon-Pharabod, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Lars Hupel, Mark Batty, Michael Greenberg Michael Norrish, Ohad Kammar, Peter Boehm, Robert Norton Sami Mäkelä, Shaked Flur Stephen Kell, Thibaut Pérami, Thomas Bauereiss, Thomas Williams, Victor Gomes, emersion. License: BSD-3-clause Files: coq-lib/coqharness.v etc/header isabelle-lib/Lem.thy isabelle-lib/LemExtraDefs.thy src/ast_util.* src/backend.* src/backend_common.* src/convert_relations.ml src/coq_backend.ml src/coq_backend_utils.ml src/debug.ml src/def_trans.* src/default_values.ml src/external_constants.ml src/finite_map.ml src/ident.* src/initial_env.* src/lexer.mll src/macro_expander.* src/main.* src/module_dependencies.* src/name.* src/nvar.* src/output.* src/parser.mly src/path.* src/pattern_syntax.* src/patterns.* src/pcombinators.* src/pp.* src/precedence.* src/process_file.* src/rename_top_level.* src/reporting.* src/reporting_basic.* src/seplist.* src/syntactic_tests.* src/target.* src/target_binding.* src/target_syntax.* src/target_trans.* src/trans.* src/typecheck.* src/typecheck_ctxt.* src/typed_ast.* src/typed_ast_syntax.* src/types.* src/tyvar.* src/util.* Copyright: 2010-2018 Dominic Mulligan, University of Cambridge 2010-2018 Francesco Zappa Nardelli, INRIA Paris-Rocquencourt 2010-2018 Gabriel Kerneis, University of Cambridge 2010-2018 Kathy Gray, University of Cambridge 2010-2018 Peter Boehm, University of Cambridge (while working on Lem) 2010-2018 Peter Sewell, University of Cambridge 2010-2018 Scott Owens, University of Kent 2010-2018 Thomas Tuerk, University of Cambridge 2010-2018 Brian Campbell, University of Edinburgh 2010-2018 Shaked Flur, University of Cambridge 2010-2018 Thomas Bauereiss, University of Cambridge 2010-2018 Stephen Kell, University of Cambridge 2010-2018 Thomas Williams 2010-2018 Lars Hupel 2010-2018 Basile Clement 2010-2018, Institut National de Recherche en Informatique et en Automatique (INRIA) License: BSD-3-clause Files: examples/cpp/cmm.lem hol-lib/lemLib.sml hol-lib/lemScript.sml tests/backends/HolDoc.* Copyright: 2011-2012 Mark Batty 2011-2012 Scott Owens 2011-2012 Jean Pichon 2011-2012 Susmit Sarkar 2011-2012 Peter Sewell 2010-2013 Dominic Mulligan, University of Cambridge 2010-2013 Francesco Zappa Nardelli, INRIA Paris-Rocquencourt 2010-2013 Gabriel Kerneis, University of Cambridge 2010-2013 Kathy Gray, University of Cambridge 2010-2013 Peter Boehm, University of Cambridge (while working on Lem) 2010-2013 Peter Sewell, University of Cambridge 2010-2013 Scott Owens, University of Kent 2010-2013 Thomas Tuerk, University of Cambridge 2010-2013 Institut National de Recherche en Informatique et en Automatique (INRIA) 2007-2008 Jade Alglave, Moscova project, INRIA Paris-Rocquencourt 2007-2008 Anthony Fox, Computer Laboratory, University of Cambridge 2007-2008 Samin Isthiaq， Microsoft Research Cambridge 2007-2008 Magnus Myreen, Computer Laboratory, University of Cambridge 2007-2008 Susmit Sarkar, Computer Laboratory, University of Cambridge 2007-2008 Peter Sewell, Computer Laboratory, University of Cambridge 2007-2008 Francesco Zappa Nardelli, Moscova project, INRIA Paris-Rocquencourt License: BSD-3-clause Files: ocaml-lib/pmap.mli ocaml-lib/pmap.ml ocaml-lib/pset.mli ocaml-lib/pset.ml ocaml-lib/pset_using_lists.ml src/ulib/batUChar.ml src/ulib/batUChar.mli src/ulib/batUTF8.ml src/ulib/batUTF8.mli Copyright: 1996 Xavier Leroy, projet Cristal, INRIA Rocquencourt License: LGPL-2-with-linking-exception Files: src/ulib/batReturn.* src/ulib/batText.ml src/ulib/batText.mli Copyright: 2008 David Teller 2012 The Batteries Included Team 2007 Mauricio Fernandez 2008 Edgar Friendly 2008 David Teller, LIFO, Universite d'Orleans 2012 The Batteries Included Team 2011 Yoriyuki Yamagata 2007 Mauricio Fernandez 2002-2004 Yamagata Yoriyuki License: LGPL-2.1+-with-linking-exception Files: debian/* Copyright: 2024 Bo YU License: BSD-3-clause License: BSD-3-clause Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The names of the authors may not be used to endorse or promote products derived from this software without specific prior written permission. . THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. License: LGPL-2 This package is free software; you can redistribute it and/or modify it under the terms of the GNU Library General Public License version 2 as published by the Free Software Foundation. . On Debian systems, the full text of the LGPL License can be found in the file `/usr/share/common-licenses/LGPL-2'. License: LGPL-2-with-linking-exception The Library is distributed under the terms of the GNU Library General Public License version 2. . On Debian systems, the complete text of the GNU Library General Public License version 2 can be found in `/usr/share/common-licenses/LGPL-2'. . As a special exception to the GNU Library General Public License, you may link, statically or dynamically, a "work that uses the Library" with a publicly distributed version of the Library to produce an executable file containing portions of the Library, and distribute that executable file under terms of your choice, without any of the additional requirements listed in clause 6 of the GNU Library General Public License. By "a publicly distributed version of the Library", we mean either the unmodified Library as distributed by INRIA, or a modified version of the Library that is distributed under the conditions defined in clause 2 of the GNU Library General Public License. This exception does not however invalidate any other reasons why the executable file might be covered by the GNU Library General Public License. License: LGPL-2.1+-with-linking-exception The Library is distributed under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1, or (at your option any later version), with the special exception on linking reported above. . As a special exception to the GNU Lesser General Public License, you may link, statically or dynamically, a "work that uses the Library" with a publicly distributed version of the Library to produce an executable file containing portions of the Library, and distribute that executable file under terms of your choice, without any of the additional requirements listed in clause 6 of the GNU Lesser General Public License. By "a publicly distributed version of the Library", we mean either the unmodified Library as distributed by the authors, or a modified version of the Library that is distributed under the conditions defined in clause 3 of the GNU Lesser General Public License. This exception does not however invalidate any other reasons why the executable file might be covered by the GNU Lesser General Public License. . The full text of the GNU Lessere General Public License version 2.1 can be found in `/usr/share/common-licenses/LGPL-2.1'.