Skip to content

chore: copyright headers #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kim-em merged 1 commit into from
Jul 2, 2025
Merged

chore: copyright headers #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions COPYRIGHT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
# Copyright Notice

This project is a derivative work based on Xavier Leroy's [EUTypes 2019 summer school course on "Proving the correctness of a compiler"](https://xavierleroy.org/courses/EUTypes-2019/). Both works are licensed under the GNU Lesser General Public License version 2.1.

This project ports the original Rocq implementation to Lean,
and adapts the pedagogical material to the new implementation.
502 changes: 502 additions & 0 deletions LICENSE.md
View file
Open in desktop

Large diffs are not rendered by default.

6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

-- This module serves as the root of the `LeroyCompilerVerificationCourse` library.
-- Import modules here that should be built as part of the library.
import LeroyCompilerVerificationCourse.Imp
Expand Down
6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse/Compil.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

import LeroyCompilerVerificationCourse.Sequences
import LeroyCompilerVerificationCourse.Imp
import Init.Data.List.Basic
Expand Down
6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse/Constprop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

import LeroyCompilerVerificationCourse.Sequences
import LeroyCompilerVerificationCourse.Imp
import Init.Data.List.Basic
Expand Down
6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse/Deadcode.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

import LeroyCompilerVerificationCourse.Sequences
import LeroyCompilerVerificationCourse.Imp
import Init.Data.List.Basic
Expand Down
6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse/Fixpoints.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

import LeroyCompilerVerificationCourse.Imp
import LeroyCompilerVerificationCourse.Constprop
import Init.WF
Expand Down
6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse/Imp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

import LeroyCompilerVerificationCourse.Sequences
set_option grind.warning false

Expand Down
6 changes: 6 additions & 0 deletions LeroyCompilerVerificationCourse/Sequences.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under LGPL 2.1 license as described in the file LICENSE.md.
Authors: Wojciech Różowski
-/

set_option grind.warning false

def infseq {α} (R : α → α → Prop) : α → Prop :=
Expand Down
4 changes: 3 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
# LeroyCompilerVerificationCourse
# LeroyCompilerVerificationCourse

This project is a Lean port of Xavier Leroy's [EUTypes 2019 summer school course on "Proving the correctness of a compiler"](https://xavierleroy.org/courses/EUTypes-2019/). The original course material was written in Coq and demonstrates formal verification techniques for compiler correctness using a simple IMP language. This Lean implementation preserves the same theoretical foundations and proof structure while adapting the formalization to Lean's theorem proving system.