diff --git a/compiler/ast_schema.json b/compiler/ast_schema.json
index a2971d23..d112a437 100644
--- a/compiler/ast_schema.json
+++ b/compiler/ast_schema.json
@@ -1217,6 +1217,7 @@
       "source_section": "8.8",
       "fields": [
         { "name": "name", "type": "Identifier", "optional": false },
+        { "name": "receiver", "type": "Option<ParameterSpecification>", "optional": true },
         { "name": "formal_part", "type": "Option<FormalPart>", "optional": true },
         { "name": "span", "type": "Span", "optional": false }
       ]
@@ -1227,6 +1228,7 @@
       "source_section": "8.8",
       "fields": [
         { "name": "name", "type": "Identifier", "optional": false },
+        { "name": "receiver", "type": "Option<ParameterSpecification>", "optional": true },
         { "name": "formal_part", "type": "Option<FormalPart>", "optional": true },
         { "name": "return_type", "type": "NodeRef<SubtypeIndication | ListTypeSpec | MapTypeSpec | GrowableArrayTypeSpec | TupleTypeSpec | OptionalTypeSpec>", "optional": false },
         { "name": "span", "type": "Span", "optional": false }
diff --git a/compiler_impl/src/safe_frontend-check_emit.adb b/compiler_impl/src/safe_frontend-check_emit.adb
index 37c20a3c..16700fd5 100644
--- a/compiler_impl/src/safe_frontend-check_emit.adb
+++ b/compiler_impl/src/safe_frontend-check_emit.adb
@@ -1962,29 +1962,35 @@ package body Safe_Frontend.Check_Emit is
       end case;
    end Statement_Node;
 
+   function Parameter_Spec_Node
+     (Param : CM.Parameter_Spec) return String
+   is
+      Names : String_Vectors.Vector;
+   begin
+      for Name of Param.Names loop
+         Names.Append (JS.Quote (Name));
+      end loop;
+      return
+        "{""node_type"":""ParameterSpecification"",""names"":"
+        & Json_List (Names)
+        & ",""is_aliased"":false,""mode"":"
+        & JS.Quote (FT.To_String (Param.Mode))
+        & ",""param_type"":"
+        & Object_Type_Node (Param.Param_Type)
+        & ",""default_expression"":null,""span"":"
+        & JS.Span_Object (Param.Span)
+        & "}";
+   end Parameter_Spec_Node;
+
    function Formal_Part_Node
      (Params : CM.Parameter_Vectors.Vector;
       Span   : FT.Source_Span) return String
    is
       Items : String_Vectors.Vector;
-      Names : String_Vectors.Vector;
    begin
       if not Params.Is_Empty then
          for Param of Params loop
-            Names.Clear;
-            for Name of Param.Names loop
-               Names.Append (JS.Quote (Name));
-            end loop;
-            Items.Append
-              ("{""node_type"":""ParameterSpecification"",""names"":"
-               & Json_List (Names)
-               & ",""is_aliased"":false,""mode"":"
-               & JS.Quote (FT.To_String (Param.Mode))
-               & ",""param_type"":"
-               & Object_Type_Node (Param.Param_Type)
-               & ",""default_expression"":null,""span"":"
-               & JS.Span_Object (Param.Span)
-               & "}");
+            Items.Append (Parameter_Spec_Node (Param));
          end loop;
       end if;
       return
@@ -2056,6 +2062,10 @@ package body Safe_Frontend.Check_Emit is
            & JS.Bool_Literal (Parsed.Is_Public)
            & ",""spec"":{""node_type"":""FunctionSpecification"",""name"":"
            & JS.Quote (Parsed.Spec.Name)
+           & ",""receiver"":"
+           & (if Parsed.Spec.Has_Receiver
+              then Parameter_Spec_Node (Parsed.Spec.Receiver)
+              else "null")
            & ",""formal_part"":"
            & (if Parsed.Spec.Params.Is_Empty then "null"
               else Formal_Part_Node (Parsed.Spec.Params, Parsed.Spec.Span))
@@ -2079,6 +2089,10 @@ package body Safe_Frontend.Check_Emit is
         & JS.Bool_Literal (Parsed.Is_Public)
         & ",""spec"":{""node_type"":""ProcedureSpecification"",""name"":"
         & JS.Quote (Parsed.Spec.Name)
+        & ",""receiver"":"
+        & (if Parsed.Spec.Has_Receiver
+           then Parameter_Spec_Node (Parsed.Spec.Receiver)
+           else "null")
         & ",""formal_part"":"
         & (if Parsed.Spec.Params.Is_Empty then "null"
            else Formal_Part_Node (Parsed.Spec.Params, Parsed.Spec.Span))
diff --git a/compiler_impl/src/safe_frontend-check_model.ads b/compiler_impl/src/safe_frontend-check_model.ads
index 2b27d2d5..479691d6 100644
--- a/compiler_impl/src/safe_frontend-check_model.ads
+++ b/compiler_impl/src/safe_frontend-check_model.ads
@@ -416,6 +416,8 @@ package Safe_Frontend.Check_Model is
    type Subprogram_Spec is record
       Kind                  : FT.UString := FT.To_UString ("");
       Name                  : FT.UString := FT.To_UString ("");
+      Has_Receiver          : Boolean := False;
+      Receiver              : Parameter_Spec;
       Params                : Parameter_Vectors.Vector;
       Has_Return_Type       : Boolean := False;
       Return_Type           : Type_Spec;
diff --git a/compiler_impl/src/safe_frontend-check_parse.adb b/compiler_impl/src/safe_frontend-check_parse.adb
index 0f65b52b..fd9af870 100644
--- a/compiler_impl/src/safe_frontend-check_parse.adb
+++ b/compiler_impl/src/safe_frontend-check_parse.adb
@@ -1490,6 +1490,7 @@ package body Safe_Frontend.Check_Parse is
       Start : constant FL.Token := Current (State);
       Name  : FL.Token;
       Result : CM.Subprogram_Spec;
+      Receiver : CM.Parameter_Spec;
       Close  : FT.Source_Span := Start.Span;
    begin
       if Current_Lower (State) = "procedure" then
@@ -1507,6 +1508,21 @@ package body Safe_Frontend.Check_Parse is
 
       Result.Kind := FT.To_UString ("function");
       Advance (State);
+
+      if Match (State, "(") then
+         Receiver := Parse_Parameter (State);
+         if Natural (Receiver.Names.Length) /= 1 then
+            Raise_Diag
+              (CM.Source_Frontend_Error
+                 (Path    => Path_String (State),
+                  Span    => Receiver.Span,
+                  Message => "method receiver must declare exactly one parameter name"));
+         end if;
+         Close := Expect (State, ")").Span;
+         Result.Has_Receiver := True;
+         Result.Receiver := Receiver;
+      end if;
+
       Name := Expect_Identifier (State);
       Result.Name := Name.Lexeme;
 
diff --git a/compiler_impl/src/safe_frontend-check_resolve.adb b/compiler_impl/src/safe_frontend-check_resolve.adb
index f8776186..b28100fe 100644
--- a/compiler_impl/src/safe_frontend-check_resolve.adb
+++ b/compiler_impl/src/safe_frontend-check_resolve.adb
@@ -3419,11 +3419,425 @@ package body Safe_Frontend.Check_Resolve is
             Message => "`print` supports only integer, string, boolean, or enum arguments"));
    end Validate_Print_Procedure_Call;
 
+   function Method_Target_Tail_Name (Name : String) return String is
+      Last_Dot : Natural := 0;
+   begin
+      for Index in reverse Name'Range loop
+         if Name (Index) = '.' then
+            Last_Dot := Index;
+            exit;
+         end if;
+      end loop;
+      if Last_Dot = 0 then
+         return Name;
+      end if;
+      return Name (Last_Dot + 1 .. Name'Last);
+   end Method_Target_Tail_Name;
+
+   function Name_Expr_From_String
+     (Name : String;
+      Span : FT.Source_Span) return CM.Expr_Access
+   is
+      Start  : Positive := Name'First;
+      Result : CM.Expr_Access := null;
+   begin
+      if Name'Length = 0 then
+         return null;
+      end if;
+
+      for Index in Name'Range loop
+         if Name (Index) = '.' then
+            declare
+               Part : constant String := Name (Start .. Index - 1);
+               Node : constant CM.Expr_Access := new CM.Expr_Node;
+            begin
+               if Result = null then
+                  Node.Kind := CM.Expr_Ident;
+                  Node.Name := FT.To_UString (Part);
+               else
+                  Node.Kind := CM.Expr_Select;
+                  Node.Prefix := Result;
+                  Node.Selector := FT.To_UString (Part);
+               end if;
+               Node.Span := Span;
+               Result := Node;
+            end;
+            Start := Index + 1;
+         end if;
+      end loop;
+
+      declare
+         Part : constant String := Name (Start .. Name'Last);
+         Node : constant CM.Expr_Access := new CM.Expr_Node;
+      begin
+         if Result = null then
+            Node.Kind := CM.Expr_Ident;
+            Node.Name := FT.To_UString (Part);
+         else
+            Node.Kind := CM.Expr_Select;
+            Node.Prefix := Result;
+            Node.Selector := FT.To_UString (Part);
+         end if;
+         Node.Span := Span;
+         return Node;
+      end;
+   end Name_Expr_From_String;
+
+   function Is_Method_Builtin_Name (Name : String) return Boolean is
+   begin
+      return Name in "append" | "pop_last" | "contains" | "get" | "set" | "remove";
+   end Is_Method_Builtin_Name;
+
+   function Function_Method_Call_Compatible
+     (Info         : Function_Info;
+      Receiver_Arg : CM.Expr_Access;
+      Extra_Args   : CM.Expr_Access_Vectors.Vector;
+      Var_Types    : Type_Maps.Map;
+      Functions    : Function_Maps.Map;
+      Type_Env     : Type_Maps.Map;
+      Const_Env    : Static_Value_Maps.Map) return Boolean
+   is
+      Receiver_Type : constant GM.Type_Descriptor :=
+        Expr_Type (Receiver_Arg, Var_Types, Functions, Type_Env);
+      function Has_Synthetic_Tail_Compatibility
+        (Source : GM.Type_Descriptor;
+         Target : GM.Type_Descriptor) return Boolean
+      is
+         Source_Base : constant GM.Type_Descriptor := Base_Type (Source, Type_Env);
+         Target_Base : constant GM.Type_Descriptor := Base_Type (Target, Type_Env);
+         Source_Tail : constant String :=
+           Method_Target_Tail_Name (UString_Value (Source_Base.Name));
+         Target_Tail : constant String :=
+           Method_Target_Tail_Name (UString_Value (Target_Base.Name));
+      begin
+         return Source_Tail'Length > 1
+           and then Target_Tail'Length > 1
+           and then Source_Tail (Source_Tail'First .. Source_Tail'First + 1) = "__"
+           and then Target_Tail (Target_Tail'First .. Target_Tail'First + 1) = "__"
+           and then FT.Lowercase (UString_Value (Source_Base.Kind)) =
+             FT.Lowercase (UString_Value (Target_Base.Kind))
+           and then Source_Tail = Target_Tail;
+      end Has_Synthetic_Tail_Compatibility;
+   begin
+      if Natural (Info.Params.Length) /= Natural (Extra_Args.Length) + 1 then
+         return False;
+      end if;
+
+      if UString_Value (Info.Params (Info.Params.First_Index).Mode) = "mut"
+        and then not Is_Assignable_Target (Receiver_Arg)
+      then
+         return False;
+      end if;
+
+      if not Compatible_Source_Expr_To_Target_Type
+        (Receiver_Arg,
+         Receiver_Type,
+         Info.Params (Info.Params.First_Index).Type_Info,
+         Var_Types,
+         Functions,
+         Type_Env,
+         Const_Env,
+         Exact_Length_Maps.Empty_Map)
+        and then not Has_Synthetic_Tail_Compatibility
+          (Receiver_Type,
+           Info.Params (Info.Params.First_Index).Type_Info)
+      then
+         return False;
+      end if;
+
+      if not Extra_Args.Is_Empty then
+         for Offset in 0 .. Natural (Extra_Args.Length) - 1 loop
+            declare
+               Param_Index : constant Positive := Info.Params.First_Index + 1 + Offset;
+               Param       : constant CM.Symbol := Info.Params (Param_Index);
+               Arg         : CM.Expr_Access := Extra_Args (Extra_Args.First_Index + Offset);
+            begin
+               if UString_Value (Param.Mode) = "mut"
+                 and then not Is_Assignable_Target (Arg)
+               then
+                  return False;
+               end if;
+
+               Arg :=
+                 Contextualize_Expr_To_Target_Type
+                   (Arg,
+                    Param.Type_Info,
+                    Var_Types,
+                    Functions,
+                    Type_Env,
+                    "");
+               if not Compatible_Source_Expr_To_Target_Type
+                 (Arg,
+                  Expr_Type (Arg, Var_Types, Functions, Type_Env),
+                  Param.Type_Info,
+                  Var_Types,
+                  Functions,
+                  Type_Env,
+                  Const_Env,
+                  Exact_Length_Maps.Empty_Map)
+                 and then not Has_Synthetic_Tail_Compatibility
+                   (Expr_Type (Arg, Var_Types, Functions, Type_Env),
+                    Param.Type_Info)
+               then
+                  return False;
+               end if;
+            end;
+         end loop;
+      end if;
+
+      return True;
+   end Function_Method_Call_Compatible;
+
+   function Builtin_Method_Call_Compatible
+     (Name         : String;
+      Receiver_Arg : CM.Expr_Access;
+      Extra_Args   : CM.Expr_Access_Vectors.Vector;
+      Var_Types    : Type_Maps.Map;
+      Functions    : Function_Maps.Map;
+      Type_Env     : Type_Maps.Map;
+      Const_Env    : Static_Value_Maps.Map) return Boolean
+   is
+      Receiver_Type : constant GM.Type_Descriptor :=
+        Expr_Type (Receiver_Arg, Var_Types, Functions, Type_Env);
+      Element_Type  : GM.Type_Descriptor;
+      Key_Type      : GM.Type_Descriptor;
+      Value_Type    : GM.Type_Descriptor;
+      Arg           : CM.Expr_Access;
+   begin
+      if Name = "append" then
+         if Natural (Extra_Args.Length) /= 1
+           or else not Is_Assignable_Target (Receiver_Arg)
+           or else not Is_Growable_Array_Type (Receiver_Type, Type_Env)
+         then
+            return False;
+         end if;
+         Element_Type := Growable_Array_Element_Type (Receiver_Type, Type_Env);
+         if not Is_Container_Element_Type_Allowed (Element_Type, Type_Env) then
+            return False;
+         end if;
+         Arg :=
+           Contextualize_Expr_To_Target_Type
+             (Extra_Args (Extra_Args.First_Index),
+              Element_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              "");
+         return
+           Compatible_Source_Expr_To_Target_Type
+             (Arg,
+              Expr_Type (Arg, Var_Types, Functions, Type_Env),
+              Element_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              Const_Env,
+              Exact_Length_Maps.Empty_Map);
+      elsif Name = "pop_last" then
+         if Natural (Extra_Args.Length) /= 0
+           or else not Is_Assignable_Target (Receiver_Arg)
+           or else not Is_Growable_Array_Type (Receiver_Type, Type_Env)
+         then
+            return False;
+         end if;
+         Element_Type := Growable_Array_Element_Type (Receiver_Type, Type_Env);
+         return Is_Container_Element_Type_Allowed (Element_Type, Type_Env);
+      elsif Name in "contains" | "get" | "remove" then
+         if Natural (Extra_Args.Length) /= 1
+           or else not Try_Map_Key_Value_Types (Receiver_Type, Type_Env, Key_Type, Value_Type)
+           or else not Is_Map_Key_Type_Allowed (Key_Type, Type_Env)
+           or else not Is_Container_Element_Type_Allowed (Value_Type, Type_Env)
+           or else (Name = "remove" and then not Is_Assignable_Target (Receiver_Arg))
+         then
+            return False;
+         end if;
+         Arg :=
+           Contextualize_Expr_To_Target_Type
+             (Extra_Args (Extra_Args.First_Index),
+              Key_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              "");
+         return
+           Compatible_Source_Expr_To_Target_Type
+             (Arg,
+              Expr_Type (Arg, Var_Types, Functions, Type_Env),
+              Key_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              Const_Env,
+              Exact_Length_Maps.Empty_Map);
+      elsif Name = "set" then
+         if Natural (Extra_Args.Length) /= 2
+           or else not Is_Assignable_Target (Receiver_Arg)
+           or else not Try_Map_Key_Value_Types (Receiver_Type, Type_Env, Key_Type, Value_Type)
+           or else not Is_Map_Key_Type_Allowed (Key_Type, Type_Env)
+           or else not Is_Container_Element_Type_Allowed (Value_Type, Type_Env)
+         then
+            return False;
+         end if;
+         Arg :=
+           Contextualize_Expr_To_Target_Type
+             (Extra_Args (Extra_Args.First_Index),
+              Key_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              "");
+         if not Compatible_Source_Expr_To_Target_Type
+           (Arg,
+            Expr_Type (Arg, Var_Types, Functions, Type_Env),
+            Key_Type,
+            Var_Types,
+            Functions,
+            Type_Env,
+            Const_Env,
+            Exact_Length_Maps.Empty_Map)
+         then
+            return False;
+         end if;
+         Arg :=
+           Contextualize_Expr_To_Target_Type
+             (Extra_Args (Extra_Args.First_Index + 1),
+              Value_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              "");
+         return
+           Compatible_Source_Expr_To_Target_Type
+             (Arg,
+              Expr_Type (Arg, Var_Types, Functions, Type_Env),
+              Value_Type,
+              Var_Types,
+              Functions,
+              Type_Env,
+              Const_Env,
+              Exact_Length_Maps.Empty_Map);
+      end if;
+
+      return False;
+   end Builtin_Method_Call_Compatible;
+
+   function Rewrite_Method_Apply
+     (Expr      : CM.Expr_Access;
+      Var_Types : Type_Maps.Map;
+      Functions : Function_Maps.Map;
+      Type_Env  : Type_Maps.Map;
+      Const_Env : Static_Value_Maps.Map) return CM.Expr_Access
+   is
+      Receiver_Arg : CM.Expr_Access := null;
+      Method_Name  : constant String :=
+        (if Expr = null
+              or else Expr.Callee = null
+              or else Expr.Callee.Kind /= CM.Expr_Select
+         then ""
+         else FT.Lowercase (UString_Value (Expr.Callee.Selector)));
+      Match_Count   : Natural := 0;
+      Match_Names   : String_Vectors.Vector;
+      Selected_Name : FT.UString := FT.To_UString ("");
+      Builtin_Visible : constant Boolean :=
+        Is_Method_Builtin_Name (Method_Name)
+        and then not Has_Function (Functions, Method_Name)
+        and then not Has_Type (Var_Types, Method_Name)
+        and then not Has_Type (Type_Env, Method_Name);
+      Result : CM.Expr_Access;
+   begin
+      if Method_Name = "" then
+         return null;
+      end if;
+
+      Receiver_Arg := Expr.Callee.Prefix;
+
+      if Has_Function (Functions, Method_Name)
+        and then Function_Method_Call_Compatible
+          (Get_Function (Functions, Method_Name),
+           Receiver_Arg,
+           Expr.Args,
+           Var_Types,
+           Functions,
+           Type_Env,
+           Const_Env)
+      then
+         Match_Count := Match_Count + 1;
+         Append_Unique_String (Match_Names, Method_Name);
+         Selected_Name := FT.To_UString (Method_Name);
+      end if;
+
+      for Cursor in Functions.Iterate loop
+         declare
+            Candidate_Name : constant String := Function_Maps.Key (Cursor);
+         begin
+            if Candidate_Name /= Method_Name
+              and then Method_Target_Tail_Name (Candidate_Name) = Method_Name
+              and then Function_Method_Call_Compatible
+                (Function_Maps.Element (Cursor),
+                 Receiver_Arg,
+                 Expr.Args,
+                 Var_Types,
+                 Functions,
+                 Type_Env,
+                 Const_Env)
+            then
+               Match_Count := Match_Count + 1;
+               Append_Unique_String (Match_Names, Candidate_Name);
+               if UString_Value (Selected_Name)'Length = 0 then
+                  Selected_Name := FT.To_UString (Candidate_Name);
+               end if;
+            end if;
+         end;
+      end loop;
+
+      if Builtin_Visible
+        and then Builtin_Method_Call_Compatible
+          (Method_Name,
+           Receiver_Arg,
+           Expr.Args,
+           Var_Types,
+           Functions,
+           Type_Env,
+           Const_Env)
+      then
+         Match_Count := Match_Count + 1;
+         Append_Unique_String (Match_Names, "builtin " & Method_Name);
+         if UString_Value (Selected_Name)'Length = 0 then
+            Selected_Name := FT.To_UString (Method_Name);
+         end if;
+      end if;
+
+      if Match_Count = 0 then
+         return null;
+      elsif Match_Count > 1 then
+         Raise_Diag
+           (CM.Source_Frontend_Error
+              (Path    => "",
+               Span    => Expr.Callee.Span,
+               Message =>
+                 "ambiguous method call `"
+                 & Method_Name
+                 & "`; compatible candidates: "
+                 & Join_String_Vector (Match_Names)));
+      end if;
+
+      Result := new CM.Expr_Node'(Expr.all);
+      Result.Kind := CM.Expr_Call;
+      Result.Callee := Name_Expr_From_String (UString_Value (Selected_Name), Expr.Callee.Span);
+      Result.Args.Clear;
+      Result.Args.Append (Receiver_Arg);
+      for Arg of Expr.Args loop
+         Result.Args.Append (Arg);
+      end loop;
+      return Result;
+   end Rewrite_Method_Apply;
+
    function Resolve_Apply
      (Expr      : CM.Expr_Access;
       Var_Types : Type_Maps.Map;
       Functions : Function_Maps.Map;
-      Type_Env  : Type_Maps.Map) return CM.Expr_Access
+      Type_Env  : Type_Maps.Map;
+      Const_Env : Static_Value_Maps.Map) return CM.Expr_Access
    is
    begin
       if Expr = null or else Expr.Kind /= CM.Expr_Apply then
@@ -3487,6 +3901,14 @@ package body Safe_Frontend.Check_Resolve is
                Result.Callee := Expr.Callee;
                Result.Args := Expr.Args;
             else
+               declare
+                  Rewritten : constant CM.Expr_Access :=
+                    Rewrite_Method_Apply (Expr, Var_Types, Functions, Type_Env, Const_Env);
+               begin
+                  if Rewritten /= null then
+                     return Rewritten;
+                  end if;
+               end;
                Prefix_Type := Expr_Type (Expr.Callee, Var_Types, Functions, Type_Env);
                if UString_Value (Prefix_Type.Kind) = "array"
                  or else Is_String_Type (Prefix_Type, Type_Env)
@@ -3560,7 +3982,7 @@ package body Safe_Frontend.Check_Resolve is
          when CM.Expr_Apply =>
             declare
                Resolved : constant CM.Expr_Access :=
-                 Resolve_Apply (Expr, Var_Types, Functions, Type_Env);
+                 Resolve_Apply (Expr, Var_Types, Functions, Type_Env, Const_Env);
             begin
                if Resolved.Kind = CM.Expr_Resolved_Index then
                   Result := new CM.Expr_Node'(Resolved.all);
@@ -6970,6 +7392,13 @@ package body Safe_Frontend.Check_Resolve is
                   return Result;
                end;
             end if;
+            if Is_Append_Builtin_Call (Expr, Var_Types, Functions, Type_Env) then
+               Raise_Diag
+                 (CM.Source_Frontend_Error
+                    (Path    => Path,
+                     Span    => (if Expr.Has_Call_Span then Expr.Call_Span else Expr.Span),
+                     Message => "`append(items, value)` mutates a writable list and must be used as a statement"));
+            end if;
             if Is_Set_Builtin_Call (Expr, Var_Types, Functions, Type_Env) then
                Raise_Diag
                  (CM.Source_Frontend_Error
@@ -9621,6 +10050,19 @@ package body Safe_Frontend.Check_Resolve is
       Result.Kind := Decl.Spec.Kind;
       Result.Span := Decl.Span;
       Result.Return_Is_Access_Def := Decl.Spec.Return_Is_Access_Def;
+      if Decl.Spec.Has_Receiver then
+         declare
+            Param_Type : constant GM.Type_Descriptor :=
+              Resolve_Type_Spec (Decl.Spec.Receiver.Param_Type, Type_Env, Const_Env, Path);
+         begin
+            Symbol.Name := Decl.Spec.Receiver.Names (Decl.Spec.Receiver.Names.First_Index);
+            Symbol.Kind := FT.To_UString ("param");
+            Symbol.Mode := Decl.Spec.Receiver.Mode;
+            Symbol.Span := Decl.Spec.Receiver.Span;
+            Symbol.Type_Info := Param_Type;
+            Result.Params.Append (Symbol);
+         end;
+      end if;
       for Param of Decl.Spec.Params loop
          declare
             Param_Type : constant GM.Type_Descriptor :=
diff --git a/docs/PR11.x-series-proposed.md b/docs/PR11.x-series-proposed.md
index 60af6251..d6ff631f 100644
--- a/docs/PR11.x-series-proposed.md
+++ b/docs/PR11.x-series-proposed.md
@@ -32,8 +32,9 @@ Dependency chain:
   proof checkpoint (`PR11.3a`).
 - PR11.8b runs as a parallel track after PR10.5 and PR10.6 and must land
   before PR11.8g and `PR11.9`.
-- PR11.8b.1 follows PR11.8b and carries the deferred channel-contract syntax
-  work separately from the proof checkpoint.
+- PR11.8b.1 followed PR11.8b and shipped the deferred channel-contract syntax
+  work in PR #140; its emitted-proof fixtures were later absorbed into
+  `PR11.8g.1` / `PR11.8g.3`.
 - PR11.8c follows PR11.8a.
 - PR11.8c.1 follows PR11.8c.
 - PR11.8c.2 follows PR11.8c.1.
@@ -654,9 +655,14 @@ debt and should remain excluded instead of being restated as missing coverage.
 
 ## PR11.8b.1: Channel Direction and Scoped-Binding Receive
 
-This follow-on milestone carries the deferred concurrency-surface syntax work
-separately from the PR11.8b proof checkpoint so parser/legality work does not
-block proof closure and proof closure does not gate syntax admission.
+Completed in PR #140.
+
+This follow-on milestone carried the deferred concurrency-surface syntax work
+separately from the PR11.8b proof checkpoint so parser/legality work did not
+block proof closure and proof closure did not gate syntax admission. Its
+representative fixtures were later absorbed into the blocking emitted-proof
+lane in `PR11.8g.1`, with the admitted runtime/select closure landing in
+`PR11.8g.3`.
 
 ### Scope
 
@@ -2174,10 +2180,19 @@ syntax as desugaring over ordinary functions.
   `function (self : my_type) do_thing` is sugar for
   `function do_thing (self : my_type)`.
 - `mut` receivers: `function (self : mut my_type) update`.
-- Method call syntax: `value.do_thing()` desugars to `do_thing(value)`.
+- Method call syntax is broad in this slice:
+  `value.do_thing(args)` desugars to `do_thing(value, args)` for any
+  visible compatible first-parameter function.
+- Imported public functions participate too, so `value.method()` may resolve
+  to `pkg.method(value)` across package boundaries.
+- Existing container builtins gain selector-call sugar automatically:
+  `items.append(v)`, `items.pop_last()`, `m.contains(k)`, `m.get(k)`,
+  `m.set(k, v)`, and `m.remove(k)`.
 - Methods are resolved statically from the receiver type. No dynamic
   dispatch.
 - Methods desugar before MIR. GNATprove sees ordinary subprograms.
+- No interface/generics/composition surface ships in `PR11.11a`; this is
+  declaration sugar plus selector-call desugaring only.
 
 ### Proof impact
 
@@ -2427,8 +2442,10 @@ PR11.8g and PR11.9 so artifact contracts freeze against a broader proved
 concurrency surface rather than only the frozen PR10 subset.
 
 **Deferred channel-contract syntax after the proof checkpoint** — PR11.8b.1
-keeps task direction clauses and scoped-binding receive separate from PR11.8b
-so parser/interface work does not block the concurrency proof closure.
+kept task direction clauses and scoped-binding receive separate from PR11.8b
+so parser/interface work did not block the concurrency proof closure; that
+split shipped in PR #140 and the resulting fixtures were later reclosed under
+`PR11.8g.1` / `PR11.8g.3`.
 
 **Value-type semantic reset after the numeric reset** — PR11.8c, PR11.8d, and
 PR11.8e deliberately continue the `PR11.8` rethink into binary arithmetic, a
diff --git a/docs/tutorial.md b/docs/tutorial.md
index 33690ab8..6fd9882f 100644
--- a/docs/tutorial.md
+++ b/docs/tutorial.md
@@ -355,6 +355,35 @@ function lookup_or_zero returns integer
       return 0;
 ```
 
+`PR11.11a` adds method syntax as sugar over the same first-parameter function
+model. You can declare a receiver explicitly:
+
+```safe
+type counter is record
+   value : integer;
+
+function (self : mut counter) bump
+   self.value = self.value + 1;
+
+function (self : counter) doubled returns integer
+   return self.value * 2;
+```
+
+And you can call any visible compatible first-parameter function that way:
+
+```safe
+function total returns integer
+   item : counter = (value = 20);
+
+   item.bump();
+   return item.doubled();
+```
+
+The same sugar applies to imported public functions and the container builtins,
+so `value.unwrap_or_zero()`, `items.append(3)`, `items.pop_last()`,
+`m.contains(key)`, `m.get(key)`, `m.set(key, value)`, and `m.remove(key)`
+all lower to the existing ordinary-call forms.
+
 ## 6. "Silver By Construction": D27 In One Page
 
 Safe's Silver level is built around a simple premise:
diff --git a/scripts/_lib/proof_inventory.py b/scripts/_lib/proof_inventory.py
index 3bebb6a9..d3284663 100644
--- a/scripts/_lib/proof_inventory.py
+++ b/scripts/_lib/proof_inventory.py
@@ -206,6 +206,13 @@ class EmittedProofExclusion:
 )
 
 
+PR11_11A_CHECKPOINT_FIXTURES = [
+    "tests/positive/pr1111a_method_syntax.safe",
+    "tests/positive/pr1111a_method_append_overload.safe",
+    "tests/build/pr1111a_builtin_methods_build.safe",
+]
+
+
 PR11_8I1_CHECKPOINT_FIXTURES = [
     "tests/positive/pr115_case_terminator.safe",
     "tests/positive/pr115_var_basic.safe",
@@ -274,6 +281,7 @@ class EmittedProofExclusion:
     + PR11_10A_CHECKPOINT_FIXTURES
     + PR11_10B_CHECKPOINT_FIXTURES
     + PR11_10C_CHECKPOINT_FIXTURES
+    + PR11_11A_CHECKPOINT_FIXTURES
     + EMITTED_PROOF_REGRESSION_FIXTURES
 )
 
diff --git a/scripts/run_proofs.py b/scripts/run_proofs.py
index 7335ee9d..cd64093c 100644
--- a/scripts/run_proofs.py
+++ b/scripts/run_proofs.py
@@ -32,6 +32,7 @@
     PR11_10B_CHECKPOINT_FIXTURES,
     PR11_10C_CHECKPOINT_FIXTURES,
     PR11_10D_CHECKPOINT_FIXTURES,
+    PR11_11A_CHECKPOINT_FIXTURES,
     PROOF_COVERAGE_ROOTS,
     iter_proof_coverage_paths,
 )
@@ -82,6 +83,7 @@ def validate_manifests() -> None:
     validate_manifest("PR11.10b checkpoint manifest", PR11_10B_CHECKPOINT_FIXTURES)
     validate_manifest("PR11.10c checkpoint manifest", PR11_10C_CHECKPOINT_FIXTURES)
     validate_manifest("PR11.10d checkpoint manifest", PR11_10D_CHECKPOINT_FIXTURES)
+    validate_manifest("PR11.11a checkpoint manifest", PR11_11A_CHECKPOINT_FIXTURES)
     validate_manifest("emitted proof regression manifest", EMITTED_PROOF_REGRESSION_FIXTURES)
     validate_manifest("emitted proof manifest", EMITTED_PROOF_FIXTURES)
     validate_manifest(
@@ -223,6 +225,8 @@ def main() -> int:
     checkpoint_10c_failures: list[tuple[str, str]] = []
     checkpoint_10d_passed = 0
     checkpoint_10d_failures: list[tuple[str, str]] = []
+    checkpoint_11a_passed = 0
+    checkpoint_11a_failures: list[tuple[str, str]] = []
     regression_passed = 0
     regression_failures: list[tuple[str, str]] = []
 
@@ -301,6 +305,11 @@ def main() -> int:
             temp_root=temp_root,
             toolchain=toolchain,
         )
+        checkpoint_11a_passed, checkpoint_11a_failures = run_fixture_group(
+            fixtures=PR11_11A_CHECKPOINT_FIXTURES,
+            temp_root=temp_root,
+            toolchain=toolchain,
+        )
         regression_passed, regression_failures = run_fixture_group(
             fixtures=EMITTED_PROOF_REGRESSION_FIXTURES,
             temp_root=temp_root,
@@ -328,6 +337,7 @@ def main() -> int:
         + checkpoint_10a_passed
         + checkpoint_10b_passed
         + checkpoint_10c_passed
+        + checkpoint_11a_passed
         + regression_passed
     )
     total_failures = (
@@ -344,6 +354,7 @@ def main() -> int:
         + checkpoint_10a_failures
         + checkpoint_10b_failures
         + checkpoint_10c_failures
+        + checkpoint_11a_failures
         + regression_failures
     )
 
@@ -431,6 +442,12 @@ def main() -> int:
         title="PR11.10d checkpoint",
         trailing_blank_line=True,
     )
+    print_summary(
+        passed=checkpoint_11a_passed,
+        failures=checkpoint_11a_failures,
+        title="PR11.11a checkpoint",
+        trailing_blank_line=True,
+    )
     print_summary(
         passed=regression_passed,
         failures=regression_failures,
diff --git a/scripts/run_tests.py b/scripts/run_tests.py
index d66acafd..7f365772 100644
--- a/scripts/run_tests.py
+++ b/scripts/run_tests.py
@@ -204,6 +204,24 @@
         REPO_ROOT / "tests" / "interfaces" / "client_map.safe",
         0,
     ),
+    (
+        "list-method",
+        REPO_ROOT / "tests" / "interfaces" / "provider_list.safe",
+        REPO_ROOT / "tests" / "interfaces" / "client_list_method.safe",
+        0,
+    ),
+    (
+        "optional-method",
+        REPO_ROOT / "tests" / "interfaces" / "provider_optional.safe",
+        REPO_ROOT / "tests" / "interfaces" / "client_optional_method.safe",
+        0,
+    ),
+    (
+        "imported-method-observe",
+        REPO_ROOT / "tests" / "interfaces" / "provider_imported_call_ownership.safe",
+        REPO_ROOT / "tests" / "interfaces" / "client_imported_method_observe.safe",
+        0,
+    ),
 ]
 
 INTERFACE_REJECT_CASES = [
@@ -213,6 +231,12 @@
         REPO_ROOT / "tests" / "interfaces" / "client_select_channel.safe",
         "PR11.9a temporarily admits select arms only on same-unit non-public channels",
     ),
+    (
+        "ambiguous-imported-method",
+        REPO_ROOT / "tests" / "interfaces" / "provider_optional.safe",
+        REPO_ROOT / "tests" / "interfaces" / "client_optional_method_ambiguous.safe",
+        "ambiguous method call `unwrap_or_zero`",
+    ),
 ]
 
 CHECK_SUCCESS_CASES = [
@@ -256,6 +280,7 @@
     REPO_ROOT / "tests" / "positive" / "pr1110a_optional_guarded.safe",
     REPO_ROOT / "tests" / "positive" / "pr1110b_list_basics.safe",
     REPO_ROOT / "tests" / "positive" / "pr1110c_map_basics.safe",
+    REPO_ROOT / "tests" / "positive" / "pr1111a_method_syntax.safe",
 ]
 
 DIAGNOSTIC_GOLDEN_CASES = [
@@ -493,6 +518,11 @@
         "3\n3\n",
         False,
     ),
+    (
+        REPO_ROOT / "tests" / "build" / "pr1111a_builtin_methods_build.safe",
+        "30\n15\n20\n2\n1\n",
+        False,
+    ),
     (
         REPO_ROOT / "tests" / "build" / "pr118d_tuple_string_build.safe",
         "ok\n",
diff --git a/spec/08-syntax-summary.md b/spec/08-syntax-summary.md
index 52561c26..3b27aae3 100644
--- a/spec/08-syntax-summary.md
+++ b/spec/08-syntax-summary.md
@@ -596,7 +596,10 @@ procedure_call_statement ::=
 
 The contextual builtins `append(items, value)`, `pop_last(items)`,
 `contains(m, key)`, `get(m, key)`, `set(m, key, value)`, and
-`remove(m, key)` use ordinary call syntax.
+`remove(m, key)` use ordinary call syntax. Under PR11.11a the same
+operations may also be written with selector-call sugar:
+`items.append(value)`, `items.pop_last()`, `m.contains(key)`,
+`m.get(key)`, `m.set(key, value)`, and `m.remove(key)`.
 
 - `append` is admitted only as a procedure-call statement on a writable
   `list of T` name.
@@ -690,7 +693,11 @@ subprogram_specification ::=
     function_specification
 
 function_specification ::=
-    'function' defining_identifier [ formal_part ] [ 'returns' subtype_indication ]
+    'function' [ receiver_parameter_clause ] defining_identifier
+        [ formal_part ] [ 'returns' subtype_indication ]
+
+receiver_parameter_clause ::=
+    '(' defining_identifier ':' [ 'mut' ] subtype_indication ')'
 
 formal_part ::=
     '(' parameter_specification { ';' parameter_specification } ')'
@@ -708,6 +715,16 @@ expression_function_declaration ::=
 designator ::=
     identifier
 
+Method-call sugar is source-level desugaring over the existing first-parameter
+function model:
+
+- `value.method(args)` rewrites to `method(value, args)` when exactly one
+  visible compatible first-parameter function or builtin exists.
+- Imported public functions may be called the same way:
+  `value.method()` may resolve to `pkg.method(value)`.
+- Bare selectors such as `.length`, `.present`, `.value`, and ordinary field
+  access keep their existing meaning unless immediately followed by `(...)`.
+
 default_expression ::=
     expression
 ```
diff --git a/tests/build/pr1111a_builtin_methods_build.safe b/tests/build/pr1111a_builtin_methods_build.safe
new file mode 100644
index 00000000..4d6e93f7
--- /dev/null
+++ b/tests/build/pr1111a_builtin_methods_build.safe
@@ -0,0 +1,63 @@
+package pr1111a_builtin_methods_build
+
+   function last_value returns integer
+      var values : list of integer = [10, 20];
+      var last : optional integer;
+
+      values.append (30);
+      last = values.pop_last ();
+      if last.present and then values.length == 2
+         return last.value;
+      else
+         return 0;
+
+   function updated_value returns integer
+      var scores : map of (integer, integer);
+      found : optional integer;
+
+      scores.set (1, 5);
+      scores.set (1, 15);
+      scores.set (2, 20);
+      found = scores.get (1);
+      if found.present
+         return found.value;
+      else
+         return 0;
+
+   function removed_value returns integer
+      var scores : map of (integer, integer);
+      removed : optional integer;
+
+      scores.set (1, 15);
+      scores.set (2, 20);
+      removed = scores.remove (2);
+      if removed.present and then scores.length == 1 and then not scores.contains (2)
+         return removed.value;
+      else
+         return 0;
+
+   function remaining_length returns integer
+      var values : list of integer = [10, 20];
+      var removed : optional integer;
+
+      values.append (30);
+      removed = values.pop_last ();
+      if removed.present
+         return values.length;
+      else
+         return 0;
+
+   function contains_flag returns integer
+      var scores : map of (integer, integer);
+
+      scores.set (1, 15);
+      if scores.contains (1)
+         return 1;
+      else
+         return 0;
+
+   print (last_value);
+   print (updated_value);
+   print (removed_value);
+   print (remaining_length);
+   print (contains_flag);
diff --git a/tests/interfaces/client_imported_method_observe.safe b/tests/interfaces/client_imported_method_observe.safe
new file mode 100644
index 00000000..af542794
--- /dev/null
+++ b/tests/interfaces/client_imported_method_observe.safe
@@ -0,0 +1,11 @@
+with provider_imported_call_ownership;
+
+package client_imported_method_observe
+
+   function total returns provider_imported_call_ownership.payload_value
+      owner : not null provider_imported_call_ownership.payload = (value = 5, link = null);
+      seen  : provider_imported_call_ownership.payload_value = 0;
+
+      owner.bump ();
+      seen = owner.read_value ();
+      return seen;
diff --git a/tests/interfaces/client_list_method.safe b/tests/interfaces/client_list_method.safe
new file mode 100644
index 00000000..2924ced9
--- /dev/null
+++ b/tests/interfaces/client_list_method.safe
@@ -0,0 +1,9 @@
+with provider_list;
+
+package client_list_method
+
+   function total returns integer
+      values : list of integer = [1, 2];
+      appended : list of integer = provider_list.append_one (values, 3);
+
+      return appended.last_or_zero ();
diff --git a/tests/interfaces/client_optional_method.safe b/tests/interfaces/client_optional_method.safe
new file mode 100644
index 00000000..37a8fb3e
--- /dev/null
+++ b/tests/interfaces/client_optional_method.safe
@@ -0,0 +1,8 @@
+with provider_optional;
+
+package client_optional_method
+
+   function total returns integer
+      value : optional integer = provider_optional.maybe_count (true);
+
+      return value.unwrap_or_zero ();
diff --git a/tests/interfaces/client_optional_method_ambiguous.safe b/tests/interfaces/client_optional_method_ambiguous.safe
new file mode 100644
index 00000000..a5582d99
--- /dev/null
+++ b/tests/interfaces/client_optional_method_ambiguous.safe
@@ -0,0 +1,11 @@
+with provider_optional;
+
+package client_optional_method_ambiguous
+
+   function unwrap_or_zero (value : optional integer) returns integer
+      return 7;
+
+   function total returns integer
+      value : optional integer = provider_optional.maybe_count (true);
+
+      return value.unwrap_or_zero ();
diff --git a/tests/negative/neg_pr1111a_append_expr.safe b/tests/negative/neg_pr1111a_append_expr.safe
new file mode 100644
index 00000000..7405daf6
--- /dev/null
+++ b/tests/negative/neg_pr1111a_append_expr.safe
@@ -0,0 +1,6 @@
+package neg_pr1111a_append_expr
+
+   function total returns integer
+      values : list of integer = [1, 2];
+
+      return values.append (3);
diff --git a/tests/negative/neg_pr1111a_mut_receiver_constant.safe b/tests/negative/neg_pr1111a_mut_receiver_constant.safe
new file mode 100644
index 00000000..566f7ddb
--- /dev/null
+++ b/tests/negative/neg_pr1111a_mut_receiver_constant.safe
@@ -0,0 +1,13 @@
+package neg_pr1111a_mut_receiver_constant
+
+   type counter is record
+      value : integer;
+
+   function (self : mut counter) bump
+      self.value = self.value + 1;
+
+   function total returns integer
+      c : constant counter = (value = 0);
+
+      c.bump ();
+      return 0;
diff --git a/tests/negative/neg_pr1111a_remove_stmt_method.safe b/tests/negative/neg_pr1111a_remove_stmt_method.safe
new file mode 100644
index 00000000..97d1f4d9
--- /dev/null
+++ b/tests/negative/neg_pr1111a_remove_stmt_method.safe
@@ -0,0 +1,7 @@
+package neg_pr1111a_remove_stmt_method
+
+   function total returns integer
+      values : map of (integer, integer);
+
+      values.remove (1);
+      return 0;
diff --git a/tests/positive/pr1111a_method_append_overload.safe b/tests/positive/pr1111a_method_append_overload.safe
new file mode 100644
index 00000000..0af7c263
--- /dev/null
+++ b/tests/positive/pr1111a_method_append_overload.safe
@@ -0,0 +1,12 @@
+package pr1111a_method_append_overload
+
+   function (self : list of integer) append (suffix : string) returns integer
+      if self.length == 2 and then suffix.length == 3
+         return 7;
+      else
+         return 0;
+
+   function total returns integer
+      values : list of integer = [1, 2];
+
+      return values.append ("Ada");
diff --git a/tests/positive/pr1111a_method_syntax.safe b/tests/positive/pr1111a_method_syntax.safe
new file mode 100644
index 00000000..cc03c954
--- /dev/null
+++ b/tests/positive/pr1111a_method_syntax.safe
@@ -0,0 +1,27 @@
+package pr1111a_method_syntax
+
+   subtype small_value is integer (0 to 100);
+
+   type counter is record
+      value : small_value;
+
+   type holder is record
+      inner : counter;
+
+   function (self : counter) doubled returns integer
+      return self.value * 2;
+
+   function (self : counter) plus (step : small_value) returns integer
+      return self.value + step;
+
+   function (self : mut counter) bump
+      self.value = self.value + 1;
+
+   function total returns integer
+      item : holder = (inner = (value = 20));
+
+      item.inner.bump();
+      if item.inner.doubled() == 42 and then item.inner.plus (1) == 22
+         return 1;
+      else
+         return 0;