diff --git a/lib/rouge/demos/hll b/lib/rouge/demos/hll
new file mode 100644
index 0000000000..62e8d3c2bd
--- /dev/null
+++ b/lib/rouge/demos/hll
@@ -0,0 +1,19 @@
+/* The pigeon holes principles
+   Taken from the specification */
+constants:
+  int NOF_PIGEONS := 10;
+  int NOF_HOLES := NOF_PIGEONS - 1;
+
+inputs:
+  bool P[NOF_PIGEONS, NOF_HOLES];
+
+definitions:
+  // For each hole there is at most one pigeon
+  a := ALL i:[0, NOF_HOLES-1], j:[0, NOF_PIGEONS-1] ALL k:[j+1, NOF_PIGEONS-1]
+         (P[j, i] -> ~P[k, i]);
+
+  // For each pigeon there is at least one hole
+  b := ALL i:[0, NOF_PIGEONS-1] SOME j:[0, NOF_HOLES-1] (P[i,j]);
+
+proof obligations:
+  ~(a & b);
diff --git a/lib/rouge/lexers/hll.rb b/lib/rouge/lexers/hll.rb
new file mode 100644
index 0000000000..6d682ced9d
--- /dev/null
+++ b/lib/rouge/lexers/hll.rb
@@ -0,0 +1,107 @@
+module Rouge
+    module Lexers
+        class HLL < RegexLexer
+            title 'HLL'
+            desc 'High Level Language'
+            tag 'hll'
+            filenames '*.hll'
+            mimetypes 'text/x-hll'
+
+            state :comment do
+                rule %r(///.*?$), Comment::Doc
+                rule %r(//[^/].*?$), Comment::Single
+                rule %r(/\*[^\*].*?\*/)m, Comment::Multiline
+                rule %r(/\*\*.*?\*/)m, Comment::Doc
+            end
+
+            state :root do
+                rule %r(\s+), Text::Whitespace
+                rule %r/\w::/, Name::Namespace
+                rule %r/"[^"]*"/, Literal::String
+                rule %r/'[^']*'/, Literal::String
+                mixin :comment
+                rule %r([(){}\[\];:,|!^]+), Punctuation
+                rule %r(:=), Punctuation
+                rule %r(\d+), Literal::Number
+                rule %r(\w+) do |m|
+                    if self.class.keywords.include?(m[0])
+                        token Keyword
+                    elsif self.class.type_keywords.include?(m[0])
+                        token Keyword::Type
+                    else
+                        token Name
+                    end
+                end
+                rule %r([~&#+\-><*=]), Operator
+            end
+
+            def self.type_keywords
+                @type_keywords ||= Set.new %w(bool int)
+            end
+            # Keywords as indicated in
+            # https://hal.science/hal-03356342v1/
+            # but without types (which are in the type_keywords value)
+            def self.keywords
+                @keywords ||= Set.new %w(
+                  ALL
+                  bin2s
+                  bin2u
+                  Blocks
+                  blocks
+                  cast
+                  CONJ
+                  constants
+                  Constants
+                  constraints
+                  Constraints
+                  declarations
+                  Declarations
+                  definitions
+                  Definitions
+                  DISJ
+                  elif
+                  else
+                  false
+                  FALSE
+                  False
+                  I
+                  if
+                  inputs
+                  Inputs
+                  lambda
+                  namespaces
+                  Namespaces
+                  obligations
+                  Obligations
+                  outputs
+                  Outputs
+                  population_count_eq
+                  population_count_gt
+                  population_count_lt
+                  pre
+                  PRE
+                  PROD
+                  proof
+                  Proof
+                  s2bin
+                  SELECT
+                  signed
+                  SOME
+                  sort
+                  struct
+                  SUM
+                  then
+                  true
+                  True
+                  TRUE
+                  tuple
+                  types
+                  Types
+                  u2bin
+                  unsigned
+                  with
+                  X)
+            end
+        end
+    end
+end
diff --git a/spec/lexers/hll_spec.rb b/spec/lexers/hll_spec.rb
new file mode 100644
index 0000000000..86a418f39e
--- /dev/null
+++ b/spec/lexers/hll_spec.rb
@@ -0,0 +1,11 @@
+describe Rouge::Lexers::HLL do
+    let(:subject) { Rouge::Lexers::HLL.new }
+
+    describe 'guessing' do
+        include Support::Guessing
+
+        it "guesses by filename" do
+            assert_guess :filename => "foo.hll"
+        end
+    end
+end
diff --git a/spec/visual/samples/hll b/spec/visual/samples/hll
new file mode 100644
index 0000000000..62e8d3c2bd
--- /dev/null
+++ b/spec/visual/samples/hll
@@ -0,0 +1,19 @@
+/* The pigeon holes principles
+   Taken from the specification */
+constants:
+  int NOF_PIGEONS := 10;
+  int NOF_HOLES := NOF_PIGEONS - 1;
+
+inputs:
+  bool P[NOF_PIGEONS, NOF_HOLES];
+
+definitions:
+  // For each hole there is at most one pigeon
+  a := ALL i:[0, NOF_HOLES-1], j:[0, NOF_PIGEONS-1] ALL k:[j+1, NOF_PIGEONS-1]
+         (P[j, i] -> ~P[k, i]);
+
+  // For each pigeon there is at least one hole
+  b := ALL i:[0, NOF_PIGEONS-1] SOME j:[0, NOF_HOLES-1] (P[i,j]);
+
+proof obligations:
+  ~(a & b);