diff --git a/src/api/dotnet/Lambda.cs b/src/api/dotnet/Lambda.cs
new file mode 100644
index 000000000..b3dc6c01c
--- /dev/null
+++ b/src/api/dotnet/Lambda.cs
@@ -0,0 +1,152 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    Lambda.cs
+
+Abstract:
+
+    Z3 Managed API: Lambda
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-19
+
+Notes:
+
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Lambda expressions.
+    /// </summary>
+    [ContractVerification(true)]
+    public class Lambda : ArrayExpr
+    {
+        /// <summary>
+        /// The number of bound variables.
+        /// </summary>
+        public uint NumBound
+        {
+            get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); }
+        }
+
+        /// <summary>
+        /// The symbols for the bound variables.
+        /// </summary>
+        public Symbol[] BoundVariableNames
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Symbol[]>() != null);
+
+                uint n = NumBound;
+                Symbol[] res = new Symbol[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = Symbol.Create(Context, Native.Z3_get_quantifier_bound_name(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// The sorts of the bound variables.
+        /// </summary>
+        public Sort[] BoundVariableSorts
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Sort[]>() != null);
+
+                uint n = NumBound;
+                Sort[] res = new Sort[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.Z3_get_quantifier_bound_sort(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// The body of the lambda.
+        /// </summary>
+        public Expr Body
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<BoolExpr>() != null);
+
+                return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// Translates (copies) the lambda to the Context <paramref name="ctx"/>.
+        /// </summary>
+        /// <param name="ctx">A context</param>
+        /// <returns>A copy of the lambda which is associated with <paramref name="ctx"/></returns>
+        new public Lambda Translate(Context ctx)
+        {
+            return (Lambda)base.Translate(ctx);
+        }
+
+        #region Internal
+        [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
+        internal Lambda(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
+            : base(ctx, IntPtr.Zero)
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(sorts != null);
+            Contract.Requires(names != null);
+            Contract.Requires(body != null);
+            Contract.Requires(sorts.Length == names.Length);
+            Contract.Requires(Contract.ForAll(sorts, s => s != null));
+            Contract.Requires(Contract.ForAll(names, n => n != null));
+            Context.CheckContextMatch<Sort>(sorts);
+            Context.CheckContextMatch<Symbol>(names);
+            Context.CheckContextMatch(body);
+
+            if (sorts.Length != names.Length)
+                throw new Z3Exception("Number of sorts does not match number of names");
+
+            NativeObject = Native.Z3_mk_lambda(ctx.nCtx, 
+                                  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+                                  Symbol.ArrayToNative(names),
+                                  body.NativeObject);
+            
+        }
+
+        [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
+        internal Lambda(Context ctx, Expr[] bound, Expr body)
+            : base(ctx, IntPtr.Zero)
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(body != null);
+
+            Contract.Requires(bound != null && bound.Length > 0 && Contract.ForAll(bound, n => n != null));
+
+            Context.CheckContextMatch<Expr>(bound);
+            Context.CheckContextMatch(body);
+
+            NativeObject = Native.Z3_mk_lambda_const(ctx.nCtx, 
+                                                 AST.ArrayLength(bound), AST.ArrayToNative(bound),
+                                                 body.NativeObject);
+        }
+
+
+        internal Lambda(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+
+#if DEBUG
+        internal override void CheckNativeObject(IntPtr obj)
+        {
+            if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
+                throw new Z3Exception("Underlying object is not a quantifier");
+            base.CheckNativeObject(obj);
+        }
+#endif
+        #endregion
+    }
+}
diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java
new file mode 100644
index 000000000..45375fb29
--- /dev/null
+++ b/src/api/java/Lambda.java
@@ -0,0 +1,134 @@
+/**
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    Lambda.java
+
+Abstract:
+
+    Z3 Java API: Lambda
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-19
+
+Notes:
+
+**/
+
+package com.microsoft.z3;
+
+import com.microsoft.z3.enumerations.Z3_ast_kind;
+
+
+/**
+ * Lambda expressions.
+*/public class Lambda extends ArrayExpr
+{
+
+    /**
+     * The number of bound variables.
+     **/
+    public int getNumBound()
+    {
+        return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * The symbols for the bound variables.
+     * 
+     * @throws Z3Exception
+     **/
+    public Symbol[] getBoundVariableNames()
+    {
+        int n = getNumBound();
+        Symbol[] res = new Symbol[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
+                    getContext().nCtx(), getNativeObject(), i));
+        return res;
+    }
+
+    /**
+     * The sorts of the bound variables.
+     * 
+     * @throws Z3Exception
+     **/
+    public Sort[] getBoundVariableSorts()
+    {
+        int n = getNumBound();
+        Sort[] res = new Sort[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
+                    getContext().nCtx(), getNativeObject(), i));
+        return res;
+    }
+
+    /**
+     * The body of the quantifier.
+     * 
+     * @throws Z3Exception
+     **/
+    public BoolExpr getBody()
+    {
+        return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
+                .nCtx(), getNativeObject()));
+    }
+
+
+    /**
+     * Translates (copies) the quantifier to the Context {@code ctx}.
+     * 
+     * @param ctx A context
+     * 
+     * @return A copy of the quantifier which is associated with {@code ctx}
+     * @throws Z3Exception on error
+     **/
+    public Lambda translate(Context ctx)
+    {
+        return (Lambda) super.translate(ctx);
+    }
+    
+       
+    public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) 
+    {
+        ctx.checkContextMatch(sorts);
+        ctx.checkContextMatch(names);
+        ctx.checkContextMatch(body);
+	
+        if (sorts.length != names.length) 
+            throw new Z3Exception("Number of sorts does not match number of names");
+	
+	
+	long nativeObject = Native.mkLambda(ctx.nCtx(), 
+					    AST.arrayLength(sorts), AST.arrayToNative(sorts),
+					    Symbol.arrayToNative(names),
+					    body.getNativeObject());
+	
+        return new Lambda(ctx, nativeObject);
+    }
+
+    /**
+     * @param ctx Context to create the lambda on.
+     * @param bound Bound variables.
+     * @param body Body of the lambda expression.
+     */
+
+    public static Lambda of(Context ctx, Expr[] bound, Expr body) {
+        ctx.checkContextMatch(body);
+
+              
+       long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
+					   AST.arrayLength(bound), AST.arrayToNative(bound),
+					   body.getNativeObject());
+       return new Lambda(ctx, nativeObject);
+   }
+
+
+    private Lambda(Context ctx, long obj)
+    {
+        super(ctx, obj);
+    }
+
+}