diff --git a/LICENSE-ARTIFACT b/LICENSE-ARTIFACT
new file mode 100644
index 0000000000000000000000000000000000000000..5f9d96fef7f13d4689a8d32f558be28250a44a89
--- /dev/null
+++ b/LICENSE-ARTIFACT
@@ -0,0 +1,85 @@
+All files in this development, excluding those in docs/, are distributed
+under the terms of the BSD license, included below.
+
+* The development is based on the Coq development of the Iris project.
+ (https://gitlab.mpi-sws.org/iris/iris)
+ Copyright: Iris developers and contributors
+* The files
+ - `theories/algebra/ordinals/set_sets.v`,
+ - `theories/algebra/ordinals/set_ordinals.v`,
+ - `theories/algebra/ordinals/set_functions.v`
+ are based on the Coq development of
+ "Formalised Set Theory: Well-Orderings and the Axiom of Choice", Dominik Kirst.
+ Available at https://www.ps.uni-saarland.de/~kirst/bachelor.php
+* The file `theories/algebra/ordinals/set_model.v` is based on the Coq development of
+ "Large Model Constructions for Second-Order ZF in Dependent Type Theory"
+ by Dominik Kirst and Gert Smolka, CPP 2018
+ See https://www.ps.uni-saarland.de/Publications/details/KirstSmolka:2017:Large-Model.html.
+ which in turn is partly based on work by Chad Brown.
+* The files in `theories/examples/safety/barrier/` are adapted from the Iris Examples project.
+ (https://gitlab.mpi-sws.org/iris/examples)
+ Copyright: Iris developers and contributors
+* The file `theories/algebra/auth_frac.v` is taken from the Perennial project https://github.com/mit-pdos/perennial
+ subject to the MIT license:
+
+ MIT License
+
+ Copyright (c) 2021
+
+ Permission is hereby granted, free of charge, to any person obtaining a copy
+ of this software and associated documentation files (the "Software"), to deal
+ in the Software without restriction, including without limitation the rights
+ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ copies of the Software, and to permit persons to whom the Software is
+ furnished to do so, subject to the following conditions:
+
+ The above copyright notice and this permission notice shall be included in
+ all copies or substantial portions of the Software.
+
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ THE SOFTWARE.
+
+* All other files, in particular the files and folders
+ - `theories/program_logic/refinement/`
+ - `theories/base_logic/satisfiable.v`
+ - `theories/bi/satisfiable.v`
+ - `theories/heap_lang/refinement_adequacy.v`
+ - `theories/heap_lang/termination_adequacy.v`
+ - `theories/examples/` except for `theories/examples/safety/`
+ - `theories/algebra/ordinals/arithmetic.v`
+ - `theories/algebra/ordinals/ord_stepindex.v`
+ - `theories/algebra/wf_IR.v`
+ - `theories/algebra/cofe_solver.v`
+are Copyright: Transfinite Iris developers.
+
+
+------------------------------------------------------------------------------
+
+ BSD LICENCE
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+ * 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.
+ * Neither the name of the <organization> nor the
+ names of its contributors may be used to endorse or promote products
+ derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 <COPYRIGHT HOLDER> 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.
diff --git a/LICENSE-CODE b/LICENSE-CODE
index 1f85999fb2575996d980ef1629737c5929d89466..7f20f6b1549435c44a468e9cc04e5ef5913dbc42 100644
--- a/LICENSE-CODE
+++ b/LICENSE-CODE
@@ -1,6 +1,61 @@
All files in this development, excluding those in docs/, are distributed
under the terms of the BSD license, included below.
+* The development is based on the Coq development of the Iris project.
+ (https://gitlab.mpi-sws.org/iris/iris)
+ Copyright: Iris developers and contributors
+* The files
+ - `theories/algebra/ordinals/set_sets.v`,
+ - `theories/algebra/ordinals/set_ordinals.v`,
+ - `theories/algebra/ordinals/set_functions.v`
+ are based on the Coq development of
+ "Formalised Set Theory: Well-Orderings and the Axiom of Choice", Dominik Kirst.
+ Available at https://www.ps.uni-saarland.de/~kirst/bachelor.php
+* The file `theories/algebra/ordinals/set_model.v` is based on the Coq development of
+ "Large Model Constructions for Second-Order ZF in Dependent Type Theory"
+ by Dominik Kirst and Gert Smolka, CPP 2018
+ See https://www.ps.uni-saarland.de/Publications/details/KirstSmolka:2017:Large-Model.html.
+ which in turn is partly based on work by Chad Brown.
+* The files in `theories/examples/safety/barrier/` are adapted from the Iris Examples project.
+ (https://gitlab.mpi-sws.org/iris/examples)
+ Copyright: Iris developers and contributors
+* The file `theories/algebra/auth_frac.v` is taken from the Perennial project https://github.com/mit-pdos/perennial
+ subject to the MIT license:
+
+ MIT License
+
+ Copyright (c) 2021
+
+ Permission is hereby granted, free of charge, to any person obtaining a copy
+ of this software and associated documentation files (the "Software"), to deal
+ in the Software without restriction, including without limitation the rights
+ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ copies of the Software, and to permit persons to whom the Software is
+ furnished to do so, subject to the following conditions:
+
+ The above copyright notice and this permission notice shall be included in
+ all copies or substantial portions of the Software.
+
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ THE SOFTWARE.
+
+* All other files, in particular the files and folders
+ - `theories/program_logic/refinement/`
+ - `theories/base_logic/satisfiable.v`
+ - `theories/bi/satisfiable.v`
+ - `theories/examples/` except for `theories/examples/safety/`
+ - `theories/algebra/ordinals/arithmetic.v`
+ - `theories/algebra/ordinals/ord_stepindex.v`
+ - `theories/algebra/wf_IR.v`
+ - `theories/algebra/cofe_solver.v`
+are Copyright: Transfinite Iris developers.
+
+
------------------------------------------------------------------------------
BSD LICENCE